1/* Title: Pure/ML/ml_process.scala 2 Author: Makarius 3 4The raw ML process. 5*/ 6 7package isabelle 8 9 10import java.io.{File => JFile} 11 12 13object ML_Process 14{ 15 def apply(options: Options, 16 logic: String = "", 17 args: List[String] = Nil, 18 dirs: List[Path] = Nil, 19 modes: List[String] = Nil, 20 raw_ml_system: Boolean = false, 21 cwd: JFile = null, 22 env: Map[String, String] = Isabelle_System.settings(), 23 redirect: Boolean = false, 24 cleanup: () => Unit = () => (), 25 sessions_structure: Option[Sessions.Structure] = None, 26 session_base: Option[Sessions.Base] = None, 27 store: Option[Sessions.Store] = None): Bash.Process = 28 { 29 val logic_name = Isabelle_System.default_logic(logic) 30 val _store = store.getOrElse(Sessions.store(options)) 31 32 val sessions_structure1 = 33 sessions_structure.getOrElse(Sessions.load_structure(options, dirs = dirs)) 34 35 val heaps: List[String] = 36 if (raw_ml_system) Nil 37 else { 38 sessions_structure1.selection(Sessions.Selection.session(logic_name)). 39 build_requirements(List(logic_name)). 40 map(a => File.platform_path(_store.the_heap(a))) 41 } 42 43 val eval_init = 44 if (heaps.isEmpty) { 45 List( 46 """ 47 fun chapter (_: string) = (); 48 fun section (_: string) = (); 49 fun subsection (_: string) = (); 50 fun subsubsection (_: string) = (); 51 fun paragraph (_: string) = (); 52 fun subparagraph (_: string) = (); 53 val ML_file = PolyML.use; 54 """, 55 if (Platform.is_windows) 56 "fun exit 0 = OS.Process.exit OS.Process.success" + 57 " | exit 1 = OS.Process.exit OS.Process.failure" + 58 " | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc))" 59 else 60 "fun exit rc = Posix.Process.exit (Word8.fromInt rc)", 61 "PolyML.Compiler.prompt1 := \"Poly/ML> \"", 62 "PolyML.Compiler.prompt2 := \"Poly/ML# \"") 63 } 64 else 65 List( 66 "(PolyML.SaveState.loadHierarchy " + 67 ML_Syntax.print_list(ML_Syntax.print_string_bytes)(heaps) + 68 "; PolyML.print_depth 0) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " + 69 ML_Syntax.print_string_bytes(": " + logic_name + "\n") + 70 "); OS.Process.exit OS.Process.failure)") 71 72 val eval_modes = 73 if (modes.isEmpty) Nil 74 else List("Print_Mode.add_modes " + ML_Syntax.print_list(ML_Syntax.print_string_bytes)(modes)) 75 76 // options 77 val isabelle_process_options = Isabelle_System.tmp_file("options") 78 Isabelle_System.chmod("600", File.path(isabelle_process_options)) 79 File.write(isabelle_process_options, YXML.string_of_body(options.encode)) 80 val env_options = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options)) 81 val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()") 82 83 // session base 84 val eval_session_base = 85 session_base match { 86 case None => Nil 87 case Some(base) => 88 def print_table(table: List[(String, String)]): String = 89 ML_Syntax.print_list( 90 ML_Syntax.print_pair( 91 ML_Syntax.print_string_bytes, ML_Syntax.print_string_bytes))(table) 92 def print_list(list: List[String]): String = 93 ML_Syntax.print_list(ML_Syntax.print_string_bytes)(list) 94 def print_sessions(list: List[(String, Position.T)]): String = 95 ML_Syntax.print_list( 96 ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_properties))(list) 97 98 List("Resources.init_session_base" + 99 " {session_positions = " + print_sessions(sessions_structure1.session_positions) + 100 ", session_directories = " + print_table(sessions_structure1.dest_session_directories) + 101 ", docs = " + print_list(base.doc_names) + 102 ", global_theories = " + print_table(base.global_theories.toList) + 103 ", loaded_theories = " + print_list(base.loaded_theories.keys) + "}") 104 } 105 106 // process 107 val eval_process = 108 if (heaps.isEmpty) 109 List("PolyML.print_depth " + ML_Syntax.print_int(options.int("ML_print_depth"))) 110 else List("Isabelle_Process.init ()") 111 112 // ISABELLE_TMP 113 val isabelle_tmp = Isabelle_System.tmp_dir("process") 114 val env_tmp = Map("ISABELLE_TMP" -> File.standard_path(isabelle_tmp)) 115 116 val ml_runtime_options = 117 { 118 val ml_options = Word.explode(Isabelle_System.getenv("ML_OPTIONS")) 119 val ml_options1 = 120 if (ml_options.exists(_.containsSlice("gcthreads"))) ml_options 121 else ml_options ::: List("--gcthreads", options.int("threads").toString) 122 val ml_options2 = 123 if (!Platform.is_windows || ml_options.exists(_.containsSlice("codepage"))) ml_options1 124 else ml_options1 ::: List("--codepage", "utf8") 125 ml_options2 126 } 127 128 // bash 129 val bash_args = 130 ml_runtime_options ::: 131 (eval_init ::: eval_modes ::: eval_options ::: eval_session_base ::: eval_process) 132 .flatMap(eval => List("--eval", eval)) ::: args 133 134 Bash.process( 135 "exec " + options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ + 136 Bash.strings(bash_args), 137 cwd = cwd, 138 env = env ++ env_options ++ env_tmp, 139 redirect = redirect, 140 cleanup = () => 141 { 142 isabelle_process_options.delete 143 Isabelle_System.rm_tree(isabelle_tmp) 144 cleanup() 145 }) 146 } 147 148 149 /* Isabelle tool wrapper */ 150 151 val isabelle_tool = Isabelle_Tool("process", "raw ML process (batch mode)", args => 152 { 153 var dirs: List[Path] = Nil 154 var eval_args: List[String] = Nil 155 var logic = Isabelle_System.getenv("ISABELLE_LOGIC") 156 var modes: List[String] = Nil 157 var options = Options.init() 158 159 val getopts = Getopts(""" 160Usage: isabelle process [OPTIONS] 161 162 Options are: 163 -T THEORY load theory 164 -d DIR include session directory 165 -e ML_EXPR evaluate ML expression on startup 166 -f ML_FILE evaluate ML file on startup 167 -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """) 168 -m MODE add print mode for output 169 -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) 170 171 Run the raw Isabelle ML process in batch mode. 172""", 173 "T:" -> (arg => 174 eval_args = eval_args ::: List("--eval", "use_thy " + ML_Syntax.print_string_bytes(arg))), 175 "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), 176 "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)), 177 "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)), 178 "l:" -> (arg => logic = arg), 179 "m:" -> (arg => modes = arg :: modes), 180 "o:" -> (arg => options = options + arg)) 181 182 val more_args = getopts(args) 183 if (args.isEmpty || more_args.nonEmpty) getopts.usage() 184 185 val rc = ML_Process(options, logic = logic, args = eval_args, dirs = dirs, modes = modes). 186 result().print_stdout.rc 187 sys.exit(rc) 188 }) 189} 190