diff --git a/src/Pure/ML/ml_process.scala b/src/Pure/ML/ml_process.scala --- a/src/Pure/ML/ml_process.scala +++ b/src/Pure/ML/ml_process.scala @@ -1,192 +1,193 @@ /* Title: Pure/ML/ml_process.scala Author: Makarius The raw ML process. */ package isabelle import java.io.{File => JFile} object ML_Process { def apply(options: Options, sessions_structure: Sessions.Structure, store: Sessions.Store, logic: String = "", raw_ml_system: Boolean = false, use_prelude: List[String] = Nil, eval_main: String = "", args: List[String] = Nil, modes: List[String] = Nil, cwd: JFile = null, env: Map[String, String] = Isabelle_System.settings(), redirect: Boolean = false, cleanup: () => Unit = () => (), session_base: Option[Sessions.Base] = None): Bash.Process = { val logic_name = Isabelle_System.default_logic(logic) val heaps: List[String] = if (raw_ml_system) Nil else { sessions_structure.selection(Sessions.Selection.session(logic_name)). build_requirements(List(logic_name)). map(a => File.platform_path(store.the_heap(a))) } val eval_init = if (heaps.isEmpty) { List( """ fun chapter (_: string) = (); fun section (_: string) = (); fun subsection (_: string) = (); fun subsubsection (_: string) = (); fun paragraph (_: string) = (); fun subparagraph (_: string) = (); val ML_file = PolyML.use; """, if (Platform.is_windows) "fun exit 0 = OS.Process.exit OS.Process.success" + " | exit 1 = OS.Process.exit OS.Process.failure" + " | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc))" else "fun exit rc = Posix.Process.exit (Word8.fromInt rc)", "PolyML.Compiler.prompt1 := \"Poly/ML> \"", "PolyML.Compiler.prompt2 := \"Poly/ML# \"") } else List( "(PolyML.SaveState.loadHierarchy " + ML_Syntax.print_list(ML_Syntax.print_string_bytes)(heaps) + "; PolyML.print_depth 0) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " + ML_Syntax.print_string_bytes(": " + logic_name + "\n") + "); OS.Process.exit OS.Process.failure)") val eval_modes = if (modes.isEmpty) Nil else List("Print_Mode.add_modes " + ML_Syntax.print_list(ML_Syntax.print_string_bytes)(modes)) // options val isabelle_process_options = Isabelle_System.tmp_file("options") Isabelle_System.chmod("600", File.path(isabelle_process_options)) File.write(isabelle_process_options, YXML.string_of_body(options.encode)) val env_options = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options)) val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()") // session base val eval_session_base = session_base match { case None => Nil case Some(base) => def print_table(table: List[(String, String)]): String = ML_Syntax.print_list( ML_Syntax.print_pair( ML_Syntax.print_string_bytes, ML_Syntax.print_string_bytes))(table) def print_list(list: List[String]): String = ML_Syntax.print_list(ML_Syntax.print_string_bytes)(list) def print_sessions(list: List[(String, Position.T)]): String = ML_Syntax.print_list( ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_properties))(list) List("Resources.init_session" + - " {session_positions = " + print_sessions(sessions_structure.session_positions) + + "{pide = false" + + ", session_positions = " + print_sessions(sessions_structure.session_positions) + ", session_directories = " + print_table(sessions_structure.dest_session_directories) + ", docs = " + print_list(base.doc_names) + ", global_theories = " + print_table(base.global_theories.toList) + ", loaded_theories = " + print_list(base.loaded_theories.keys) + "}") } // process val eval_process = proper_string(eval_main).getOrElse( if (heaps.isEmpty) { "PolyML.print_depth " + ML_Syntax.print_int(options.int("ML_print_depth")) } else "Isabelle_Process.init ()") // ISABELLE_TMP val isabelle_tmp = Isabelle_System.tmp_dir("process") val env_tmp = Map("ISABELLE_TMP" -> File.standard_path(isabelle_tmp)) val ml_runtime_options = { val ml_options = Word.explode(Isabelle_System.getenv("ML_OPTIONS")) val ml_options1 = if (ml_options.exists(_.containsSlice("gcthreads"))) ml_options else ml_options ::: List("--gcthreads", options.int("threads").toString) val ml_options2 = if (!Platform.is_windows || ml_options.exists(_.containsSlice("codepage"))) ml_options1 else ml_options1 ::: List("--codepage", "utf8") ml_options2 } // bash val bash_args = ml_runtime_options ::: (eval_init ::: eval_modes ::: eval_options ::: eval_session_base).flatMap(List("--eval", _)) ::: use_prelude.flatMap(List("--use", _)) ::: List("--eval", eval_process) ::: args Bash.process( "exec " + options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ + Bash.strings(bash_args), cwd = cwd, env = env ++ env_options ++ env_tmp, redirect = redirect, cleanup = () => { isabelle_process_options.delete Isabelle_System.rm_tree(isabelle_tmp) cleanup() }) } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("process", "raw ML process (batch mode)", args => { var dirs: List[Path] = Nil var eval_args: List[String] = Nil var logic = Isabelle_System.getenv("ISABELLE_LOGIC") var modes: List[String] = Nil var options = Options.init() val getopts = Getopts(""" Usage: isabelle process [OPTIONS] Options are: -T THEORY load theory -d DIR include session directory -e ML_EXPR evaluate ML expression on startup -f ML_FILE evaluate ML file on startup -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """) -m MODE add print mode for output -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) Run the raw Isabelle ML process in batch mode. """, "T:" -> (arg => eval_args = eval_args ::: List("--eval", "use_thy " + ML_Syntax.print_string_bytes(arg))), "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)), "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)), "l:" -> (arg => logic = arg), "m:" -> (arg => modes = arg :: modes), "o:" -> (arg => options = options + arg)) val more_args = getopts(args) if (args.isEmpty || more_args.nonEmpty) getopts.usage() val sessions_structure = Sessions.load_structure(options, dirs = dirs) val store = Sessions.store(options) val rc = ML_Process(options, sessions_structure, store, logic = logic, args = eval_args, modes = modes) .result().print_stdout.rc sys.exit(rc) }) } diff --git a/src/Pure/PIDE/protocol.ML b/src/Pure/PIDE/protocol.ML --- a/src/Pure/PIDE/protocol.ML +++ b/src/Pure/PIDE/protocol.ML @@ -1,175 +1,176 @@ (* Title: Pure/PIDE/protocol.ML Author: Makarius Protocol message formats for interactive proof documents. *) structure Protocol: sig end = struct val _ = Isabelle_Process.protocol_command "Prover.echo" (fn args => List.app writeln args); val _ = Isabelle_Process.protocol_command "Prover.options" (fn [options_yxml] => (Options.set_default (Options.decode (YXML.parse_body options_yxml)); Isabelle_Process.init_options_interactive ())); val _ = Isabelle_Process.protocol_command "Prover.init_session" (fn [session_positions_yxml, session_directories_yxml, doc_names_yxml, global_theories_yxml, loaded_theories_yxml] => let val decode_table = YXML.parse_body #> let open XML.Decode in list (pair string string) end; val decode_list = YXML.parse_body #> let open XML.Decode in list string end; val decode_sessions = YXML.parse_body #> let open XML.Decode in list (pair string properties) end; in Resources.init_session - {session_positions = decode_sessions session_positions_yxml, + {pide = true, + session_positions = decode_sessions session_positions_yxml, session_directories = decode_table session_directories_yxml, docs = decode_list doc_names_yxml, global_theories = decode_table global_theories_yxml, loaded_theories = decode_list loaded_theories_yxml} end); val _ = Isabelle_Process.protocol_command "Document.define_blob" (fn [digest, content] => Document.change_state (Document.define_blob digest content)); fun decode_command id name blobs_xml toks_xml sources : Document.command = let open XML.Decode; val (blobs_digests, blobs_index) = blobs_xml |> let val message = YXML.string_of_body o Protocol_Message.command_positions id; in pair (list (variant [fn ([], a) => Exn.Res (pair string (option string) a), fn ([], a) => Exn.Exn (ERROR (message a))])) int end; val toks = list (pair int int) toks_xml; in {command_id = Document_ID.parse id, name = name, blobs_digests = blobs_digests, blobs_index = blobs_index, tokens = toks ~~ sources} end; fun commands_accepted ids = Output.protocol_message Markup.commands_accepted [XML.Text (space_implode "," ids)]; val _ = Isabelle_Process.protocol_command "Document.define_command" (fn id :: name :: blobs :: toks :: sources => let val command = decode_command id name (YXML.parse_body blobs) (YXML.parse_body toks) sources; val _ = Document.change_state (Document.define_command command); in commands_accepted [id] end); val _ = Isabelle_Process.protocol_command "Document.define_commands" (fn args => let fun decode arg = let open XML.Decode; val (id, (name, (blobs_xml, (toks_xml, sources)))) = pair string (pair string (pair I (pair I (list string)))) (YXML.parse_body arg); in decode_command id name blobs_xml toks_xml sources end; val commands = map decode args; val _ = Document.change_state (fold Document.define_command commands); in commands_accepted (map (Value.print_int o #command_id) commands) end); val _ = Isabelle_Process.protocol_command "Document.discontinue_execution" (fn [] => Execution.discontinue ()); val _ = Isabelle_Process.protocol_command "Document.cancel_exec" (fn [exec_id] => Execution.cancel (Document_ID.parse exec_id)); val _ = Isabelle_Process.protocol_command "Document.update" (Future.task_context "Document.update" (Future.new_group NONE) (fn old_id_string :: new_id_string :: consolidate_yxml :: edits_yxml => Document.change_state (fn state => let val old_id = Document_ID.parse old_id_string; val new_id = Document_ID.parse new_id_string; val consolidate = YXML.parse_body consolidate_yxml |> let open XML.Decode in list string end; val edits = edits_yxml |> map (YXML.parse_body #> let open XML.Decode in pair string (variant [fn ([], a) => Document.Edits (list (pair (option int) (option int)) a), fn ([], a) => let val (master, (name, (imports, (keywords, errors)))) = pair string (pair string (pair (list string) (pair (list (pair string (pair (pair string (list string)) (list string)))) (list YXML.string_of_body)))) a; val imports' = map (rpair Position.none) imports; val keywords' = map (fn (x, y) => ((x, Position.none), y)) keywords; val header = Thy_Header.make (name, Position.none) imports' keywords'; in Document.Deps {master = master, header = header, errors = errors} end, fn (a :: b, c) => Document.Perspective (bool_atom a, map int_atom b, list (pair int (pair string (list string))) c)]) end); val _ = Execution.discontinue (); val (edited, removed, assign_update, state') = Document.update old_id new_id edits consolidate state; val _ = (singleton o Future.forks) {name = "Document.update/remove", group = NONE, deps = Execution.snapshot removed, pri = Task_Queue.urgent_pri + 2, interrupts = false} (fn () => (Execution.purge removed; List.app Isabelle_Process.reset_tracing removed)); val _ = Output.protocol_message Markup.assign_update ((new_id, edited, assign_update) |> let open XML.Encode; fun encode_upd (a, bs) = string (space_implode "," (map Value.print_int (a :: bs))); in triple int (list string) (list encode_upd) end); in Document.start_execution state' end))); val _ = Isabelle_Process.protocol_command "Document.remove_versions" (fn [versions_yxml] => Document.change_state (fn state => let val versions = YXML.parse_body versions_yxml |> let open XML.Decode in list int end; val state1 = Document.remove_versions versions state; val _ = Output.protocol_message Markup.removed_versions [XML.Text (versions_yxml)]; in state1 end)); val _ = Isabelle_Process.protocol_command "Document.dialog_result" (fn [serial, result] => Active.dialog_result (Value.parse_int serial) result handle exn => if Exn.is_interrupt exn then () (*sic!*) else Exn.reraise exn); val _ = Isabelle_Process.protocol_command "ML_Heap.share_common_data" (fn [] => ML_Heap.share_common_data ()); end; diff --git a/src/Pure/PIDE/resources.ML b/src/Pure/PIDE/resources.ML --- a/src/Pure/PIDE/resources.ML +++ b/src/Pure/PIDE/resources.ML @@ -1,320 +1,327 @@ (* Title: Pure/PIDE/resources.ML Author: Makarius Resources for theories and auxiliary files. *) signature RESOURCES = sig val default_qualifier: string val init_session: - {session_positions: (string * Properties.T) list, + {pide: bool, + session_positions: (string * Properties.T) list, session_directories: (string * string) list, docs: string list, global_theories: (string * string) list, loaded_theories: string list} -> unit val finish_session_base: unit -> unit + val is_pide: unit -> bool val global_theory: string -> string option val loaded_theory: string -> bool val check_session: Proof.context -> string * Position.T -> string val check_doc: Proof.context -> string * Position.T -> string val master_directory: theory -> Path.T val imports_of: theory -> (string * Position.T) list val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory val thy_path: Path.T -> Path.T val theory_qualifier: string -> string val find_theory_file: string -> Path.T option val import_name: string -> Path.T -> string -> {node_name: Path.T, master_dir: Path.T, theory_name: string} val check_thy: Path.T -> string -> {master: Path.T * SHA1.digest, text: string, theory_pos: Position.T, imports: (string * Position.T) list, keywords: Thy_Header.keywords} val parse_files: string -> (theory -> Token.file list) parser val provide: Path.T * SHA1.digest -> theory -> theory val provide_file: Token.file -> theory -> theory val provide_parse_files: string -> (theory -> Token.file list * theory) parser val loaded_files_current: theory -> bool val check_path: Proof.context -> Path.T option -> string * Position.T -> Path.T val check_file: Proof.context -> Path.T option -> string * Position.T -> Path.T val check_dir: Proof.context -> Path.T option -> string * Position.T -> Path.T end; structure Resources: RESOURCES = struct (* session base *) val default_qualifier = "Draft"; type entry = {pos: Position.T, serial: serial}; fun make_entry props : entry = {pos = Position.of_properties props, serial = serial ()}; val empty_session_base = - {session_positions = []: (string * entry) list, + {pide = false, + session_positions = []: (string * entry) list, session_directories = Symtab.empty: Path.T list Symtab.table, docs = []: (string * entry) list, global_theories = Symtab.empty: string Symtab.table, loaded_theories = Symtab.empty: unit Symtab.table}; val global_session_base = Synchronized.var "Sessions.base" empty_session_base; fun init_session - {session_positions, session_directories, docs, global_theories, loaded_theories} = + {pide, session_positions, session_directories, docs, global_theories, loaded_theories} = Synchronized.change global_session_base (fn _ => - {session_positions = sort_by #1 (map (apsnd make_entry) session_positions), + {pide = pide, + session_positions = sort_by #1 (map (apsnd make_entry) session_positions), session_directories = fold_rev (fn (dir, name) => Symtab.cons_list (name, Path.explode dir)) session_directories Symtab.empty, docs = sort_by #1 (map (apsnd make_entry o rpair []) docs), global_theories = Symtab.make global_theories, loaded_theories = Symtab.make_set loaded_theories}); fun finish_session_base () = Synchronized.change global_session_base (fn {global_theories, loaded_theories, ...} => - {session_positions = [], + {pide = false, + session_positions = [], session_directories = Symtab.empty, docs = [], global_theories = global_theories, loaded_theories = loaded_theories}); fun get_session_base f = f (Synchronized.value global_session_base); +fun is_pide () = get_session_base #pide; + fun global_theory a = Symtab.lookup (get_session_base #global_theories) a; fun loaded_theory a = Symtab.defined (get_session_base #loaded_theories) a; fun check_name which kind markup ctxt (name, pos) = let val entries = get_session_base which in (case AList.lookup (op =) entries name of SOME entry => (Context_Position.report ctxt pos (markup name entry); name) | NONE => let val completion_report = Completion.make_report (name, pos) (fn completed => entries |> map #1 |> filter completed |> sort_strings |> map (fn a => (a, (kind, a)))); in error ("Bad " ^ kind ^ " " ^ quote name ^ Position.here pos ^ completion_report) end) end; fun markup_session name {pos, serial} = Markup.properties (Position.entity_properties_of false serial pos) (Markup.entity Markup.sessionN name); val check_session = check_name #session_positions "session" markup_session; val check_doc = check_name #docs "documentation" (fn name => fn _ => Markup.doc name); (* manage source files *) type files = {master_dir: Path.T, (*master directory of theory source*) imports: (string * Position.T) list, (*source specification of imports*) provided: (Path.T * SHA1.digest) list}; (*source path, digest*) fun make_files (master_dir, imports, provided): files = {master_dir = master_dir, imports = imports, provided = provided}; structure Files = Theory_Data ( type T = files; val empty = make_files (Path.current, [], []); fun extend _ = empty; fun merge _ = empty; ); fun map_files f = Files.map (fn {master_dir, imports, provided} => make_files (f (master_dir, imports, provided))); val master_directory = #master_dir o Files.get; val imports_of = #imports o Files.get; fun begin_theory master_dir {name, imports, keywords} parents = Theory.begin_theory name parents |> map_files (fn _ => (Path.explode (Path.smart_implode master_dir), imports, [])) |> Thy_Header.add_keywords keywords; (* theory files *) val thy_path = Path.ext "thy"; fun theory_qualifier theory = (case global_theory theory of SOME qualifier => qualifier | NONE => Long_Name.qualifier theory); fun theory_name qualifier theory = if Long_Name.is_qualified theory orelse is_some (global_theory theory) then theory else Long_Name.qualify qualifier theory; fun find_theory_file thy_name = let val thy_file = thy_path (Path.basic (Long_Name.base_name thy_name)); val session = theory_qualifier thy_name; val dirs = Symtab.lookup_list (get_session_base #session_directories) session; in dirs |> get_first (fn dir => let val path = Path.append dir thy_file in if File.is_file path then SOME path else NONE end) end; fun make_theory_node node_name theory = {node_name = node_name, master_dir = Path.dir node_name, theory_name = theory}; fun loaded_theory_node theory = {node_name = Path.basic theory, master_dir = Path.current, theory_name = theory}; fun import_name qualifier dir s = let val theory = theory_name qualifier (Thy_Header.import_name s); fun theory_node () = make_theory_node (File.full_path dir (thy_path (Path.expand (Path.explode s)))) theory; in if not (Thy_Header.is_base_name s) then theory_node () else if loaded_theory theory then loaded_theory_node theory else (case find_theory_file theory of SOME node_name => make_theory_node node_name theory | NONE => if Long_Name.is_qualified s then loaded_theory_node theory else theory_node ()) end; fun check_file dir file = File.check_file (File.full_path dir file); fun check_thy dir thy_name = let val thy_base_name = Long_Name.base_name thy_name; val master_file = (case find_theory_file thy_name of SOME path => check_file Path.current path | NONE => check_file dir (thy_path (Path.basic thy_base_name))); val text = File.read master_file; val {name = (name, pos), imports, keywords} = Thy_Header.read (Path.position master_file) text; val _ = thy_base_name <> name andalso error ("Bad theory name " ^ quote name ^ " for file " ^ Path.print (Path.base master_file) ^ Position.here pos); in {master = (master_file, SHA1.digest text), text = text, theory_pos = pos, imports = imports, keywords = keywords} end; (* load files *) fun parse_files cmd = Scan.ahead Parse.not_eof -- Parse.path >> (fn (tok, name) => fn thy => (case Token.get_files tok of [] => let val keywords = Thy_Header.get_keywords thy; val master_dir = master_directory thy; val pos = Token.pos_of tok; val src_paths = Keyword.command_files keywords cmd (Path.explode name); in map (Command.read_file master_dir pos) src_paths end | files => map Exn.release files)); fun provide (src_path, id) = map_files (fn (master_dir, imports, provided) => if AList.defined (op =) provided src_path then error ("Duplicate use of source file: " ^ Path.print src_path) else (master_dir, imports, (src_path, id) :: provided)); fun provide_file (file: Token.file) = provide (#src_path file, #digest file); fun provide_parse_files cmd = parse_files cmd >> (fn files => fn thy => let val fs = files thy; val thy' = fold (fn {src_path, digest, ...} => provide (src_path, digest)) fs thy; in (fs, thy') end); fun load_file thy src_path = let val full_path = check_file (master_directory thy) src_path; val text = File.read full_path; val id = SHA1.digest text; in ((full_path, id), text) end; fun loaded_files_current thy = #provided (Files.get thy) |> forall (fn (src_path, id) => (case try (load_file thy) src_path of NONE => false | SOME ((_, id'), _) => id = id')); (* formal check *) fun formal_check check_file ctxt opt_dir (name, pos) = let fun err msg = error (msg ^ Position.here pos); val _ = Context_Position.report ctxt pos Markup.language_path; val dir = (case opt_dir of SOME dir => dir | NONE => master_directory (Proof_Context.theory_of ctxt)); val path = Path.append dir (Path.explode name) handle ERROR msg => err msg; val _ = Path.expand path handle ERROR msg => err msg; val _ = Context_Position.report ctxt pos (Markup.path (Path.smart_implode path)); val _ = check_file path handle ERROR msg => err msg; in path end; val check_path = formal_check I; val check_file = formal_check File.check_file; val check_dir = formal_check File.check_dir; (* antiquotations *) local fun document_antiq (check: Proof.context -> Path.T option -> string * Position.T -> Path.T) = Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, (name, pos)) => let val _ = check ctxt NONE (name, pos); val latex = space_explode "/" name |> map Latex.output_ascii |> space_implode (Latex.output_ascii "/" ^ "\\discretionary{}{}{}"); in Latex.enclose_block "\\isatt{" "}" [Latex.string latex] end); fun ML_antiq check = Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, (name, pos)) => check ctxt (SOME Path.current) (name, pos) |> ML_Syntax.print_path); in val _ = Theory.setup (Thy_Output.antiquotation_verbatim_embedded \<^binding>\session\ (Scan.lift Parse.embedded_position) check_session #> Thy_Output.antiquotation_verbatim_embedded \<^binding>\doc\ (Scan.lift Parse.embedded_position) check_doc #> Thy_Output.antiquotation_raw_embedded \<^binding>\path\ (document_antiq check_path) (K I) #> Thy_Output.antiquotation_raw_embedded \<^binding>\file\ (document_antiq check_file) (K I) #> Thy_Output.antiquotation_raw_embedded \<^binding>\dir\ (document_antiq check_dir) (K I) #> ML_Antiquotation.value_embedded \<^binding>\path\ (ML_antiq check_path) #> ML_Antiquotation.value_embedded \<^binding>\file\ (ML_antiq check_file) #> ML_Antiquotation.value_embedded \<^binding>\dir\ (ML_antiq check_dir) #> ML_Antiquotation.value_embedded \<^binding>\path_binding\ (Scan.lift (Parse.position Parse.path) >> (ML_Syntax.print_path_binding o Path.explode_binding)) #> ML_Antiquotation.value \<^binding>\master_dir\ (Args.theory >> (ML_Syntax.print_path o master_directory))); end; end; diff --git a/src/Pure/System/scala.ML b/src/Pure/System/scala.ML --- a/src/Pure/System/scala.ML +++ b/src/Pure/System/scala.ML @@ -1,82 +1,83 @@ (* Title: Pure/System/scala.ML Author: Makarius Support for Scala at runtime. *) signature SCALA = sig val promise_function: string -> string -> string future val function: string -> string -> string exception Null val check: string -> unit end; structure Scala: SCALA = struct (** invoke Scala functions from ML **) val _ = Session.protocol_handler "isabelle.Scala"; (* pending promises *) val new_id = string_of_int o Counter.make (); val promises = Synchronized.var "Scala.promises" (Symtab.empty: string future Symtab.table); (* invoke function *) fun promise_function name arg = let + val _ = if Resources.is_pide () then () else raise Fail "PIDE session required"; val id = new_id (); fun abort () = Output.protocol_message (Markup.cancel_scala id) []; val promise = Future.promise_name "invoke_scala" abort : string future; val _ = Synchronized.change promises (Symtab.update (id, promise)); val _ = Output.protocol_message (Markup.invoke_scala name id) [XML.Text arg]; in promise end; fun function name arg = Future.join (promise_function name arg); (* fulfill *) exception Null; fun fulfill id tag res = let val result = (case tag of "0" => Exn.Exn Null | "1" => Exn.Res res | "2" => Exn.Exn (ERROR res) | "3" => Exn.Exn (Fail res) | "4" => Exn.Exn Exn.Interrupt | _ => raise Fail "Bad tag"); val promise = Synchronized.change_result promises (fn tab => (the (Symtab.lookup tab id), Symtab.delete id tab)); val _ = Future.fulfill_result promise result; in () end; val _ = Isabelle_Process.protocol_command "Scala.fulfill" (fn [id, tag, res] => fulfill id tag res handle exn => if Exn.is_interrupt exn then () else Exn.reraise exn); (** check source snippet **) fun check source = let val errors = function "scala_check" source |> YXML.parse_body |> let open XML.Decode in list string end in if null errors then () else error (cat_lines errors) end; end; diff --git a/src/Pure/Tools/build.ML b/src/Pure/Tools/build.ML --- a/src/Pure/Tools/build.ML +++ b/src/Pure/Tools/build.ML @@ -1,270 +1,272 @@ (* Title: Pure/Tools/build.ML Author: Makarius Build Isabelle sessions. *) signature BUILD = sig val build: string -> unit end; structure Build: BUILD = struct (* command timings *) type timings = ((string * Time.time) Inttab.table) Symtab.table; (*file -> offset -> name, time*) val empty_timings: timings = Symtab.empty; fun update_timings props = (case Markup.parse_command_timing_properties props of SOME ({file, offset, name}, time) => Symtab.map_default (file, Inttab.empty) (Inttab.map_default (offset, (name, time)) (fn (_, t) => (name, t + time))) | NONE => I); fun approximative_id name pos = (case (Position.file_of pos, Position.offset_of pos) of (SOME file, SOME offset) => if name = "" then NONE else SOME {file = file, offset = offset, name = name} | _ => NONE); fun get_timings timings tr = (case approximative_id (Toplevel.name_of tr) (Toplevel.pos_of tr) of SOME {file, offset, name} => (case Symtab.lookup timings file of SOME offsets => (case Inttab.lookup offsets offset of SOME (name', time) => if name = name' then SOME time else NONE | NONE => NONE) | NONE => NONE) | NONE => NONE) |> the_default Time.zeroTime; (* session timing *) fun session_timing session_name verbose f x = let val start = Timing.start (); val y = f x; val timing = Timing.result start; val threads = string_of_int (Multithreading.max_threads ()); val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing) |> Real.fmt (StringCvt.FIX (SOME 2)); val timing_props = [("threads", threads)] @ Markup.timing_properties timing @ [("factor", factor)]; val _ = Protocol_Message.marker "Timing" timing_props; val _ = if verbose then Output.physical_stderr ("Timing " ^ session_name ^ " (" ^ threads ^ " threads, " ^ Timing.message timing ^ ", factor " ^ factor ^ ")\n") else (); in y end; (* protocol messages *) fun protocol_message props output = (case props of function :: args => if function = Markup.ML_statistics orelse function = Markup.task_statistics then Protocol_Message.marker (#2 function) args else if function = Markup.command_timing then let val name = the_default "" (Properties.get args Markup.nameN); val pos = Position.of_properties args; val {elapsed, ...} = Markup.parse_timing_properties args; val is_significant = Timing.is_relevant_time elapsed andalso elapsed >= Options.default_seconds "command_timing_threshold"; in if is_significant then (case approximative_id name pos of SOME id => Protocol_Message.marker (#2 function) (Markup.command_timing_properties id elapsed) | NONE => ()) else () end else if function = Markup.theory_timing then Protocol_Message.marker (#2 function) args else (case Markup.dest_loading_theory props of SOME name => Protocol_Message.marker_text "loading_theory" name | NONE => Export.protocol_message props output) | [] => raise Output.Protocol_Message props); (* build theories *) fun build_theories symbols bibtex_entries last_timing qualifier master_dir (options, thys) = let val context = {options = options, symbols = symbols, bibtex_entries = bibtex_entries, last_timing = last_timing}; val condition = space_explode "," (Options.string options "condition"); val conds = filter_out (can getenv_strict) condition; in if null conds then (Options.set_default options; Isabelle_Process.init_options (); Future.fork I; (Thy_Info.use_theories context qualifier master_dir |> (case Options.string options "profiling" of "" => I | "time" => profile_time | "allocations" => profile_allocations | bad => error ("Bad profiling option: " ^ quote bad)) |> Unsynchronized.setmp print_mode (space_explode "," (Options.string options "print_mode") @ print_mode_value ())) thys) else Output.physical_stderr ("Skipping theories " ^ commas_quote (map #1 thys) ^ " (undefined " ^ commas conds ^ ")\n") end; (* build session *) datatype args = Args of - {symbol_codes: (string * int) list, + {pide: bool, + symbol_codes: (string * int) list, command_timings: Properties.T list, verbose: bool, browser_info: Path.T, document_files: (Path.T * Path.T) list, graph_file: Path.T, parent_name: string, chapter: string, session_name: string, master_dir: Path.T, theories: (Options.T * (string * Position.T) list) list, session_positions: (string * Properties.T) list, session_directories: (string * string) list, doc_names: string list, global_theories: (string * string) list, loaded_theories: string list, bibtex_entries: string list}; -fun decode_args yxml = +fun decode_args pide yxml = let open XML.Decode; val position = Position.of_properties o properties; val (symbol_codes, (command_timings, (verbose, (browser_info, (document_files, (graph_file, (parent_name, (chapter, (session_name, (master_dir, (theories, (session_positions, (session_directories, (doc_names, (global_theories, (loaded_theories, bibtex_entries)))))))))))))))) = pair (list (pair string int)) (pair (list properties) (pair bool (pair string (pair (list (pair string string)) (pair string (pair string (pair string (pair string (pair string (pair (((list (pair Options.decode (list (pair string position)))))) (pair (list (pair string properties)) (pair (list (pair string string)) (pair (list string) (pair (list (pair string string)) (pair (list string) (list string)))))))))))))))) (YXML.parse_body yxml); in - Args {symbol_codes = symbol_codes, command_timings = command_timings, + Args {pide = pide, symbol_codes = symbol_codes, command_timings = command_timings, verbose = verbose, browser_info = Path.explode browser_info, document_files = map (apply2 Path.explode) document_files, graph_file = Path.explode graph_file, parent_name = parent_name, chapter = chapter, session_name = session_name, master_dir = Path.explode master_dir, theories = theories, session_positions = session_positions, session_directories = session_directories, doc_names = doc_names, global_theories = global_theories, loaded_theories = loaded_theories, bibtex_entries = bibtex_entries} end; -fun build_session (Args {symbol_codes, command_timings, verbose, browser_info, document_files, +fun build_session (Args {pide, symbol_codes, command_timings, verbose, browser_info, document_files, graph_file, parent_name, chapter, session_name, master_dir, theories, session_positions, session_directories, doc_names, global_theories, loaded_theories, bibtex_entries}) = let val symbols = HTML.make_symbols symbol_codes; val _ = Resources.init_session - {session_positions = session_positions, + {pide = pide, + session_positions = session_positions, session_directories = session_directories, docs = doc_names, global_theories = global_theories, loaded_theories = loaded_theories}; val _ = Session.init symbols (Options.default_bool "browser_info") browser_info (Options.default_string "document") (Options.default_string "document_output") (Present.document_variants (Options.default ())) document_files graph_file parent_name (chapter, session_name) verbose; val last_timing = get_timings (fold update_timings command_timings empty_timings); val res1 = theories |> (List.app (build_theories symbols bibtex_entries last_timing session_name master_dir) |> session_timing session_name verbose |> Exn.capture); val res2 = Exn.capture Session.finish (); val _ = Resources.finish_session_base (); val _ = Par_Exn.release_all [res1, res2]; val _ = if session_name = Context.PureN then Theory.install_pure (Thy_Info.get_theory Context.PureN) else (); in () end; (* command-line tool *) fun inline_errors exn = Runtime.exn_message_list exn |> List.app (fn msg => Protocol_Message.marker_text "error_message" (YXML.content_of msg)); fun build args_file = let val _ = SHA1.test_samples (); val _ = Options.load_default (); val _ = Isabelle_Process.init_options (); - val args = decode_args (File.read (Path.explode args_file)); + val args = decode_args false (File.read (Path.explode args_file)); val _ = Unsynchronized.setmp Private_Output.protocol_message_fn protocol_message build_session args handle exn => (inline_errors exn; Exn.reraise exn); val _ = Private_Output.protocol_message_fn := Output.protocol_message_undefined; val _ = Options.reset_default (); in () end; (* PIDE version *) fun build_session_finished errs = XML.Encode.list XML.Encode.string errs |> Output.protocol_message Markup.build_session_finished; val _ = Isabelle_Process.protocol_command "build_session" (fn [args_yxml] => let - val args = decode_args args_yxml; + val args = decode_args true args_yxml; val errs = Future.interruptible_task (fn () => (build_session args; [])) () handle exn => (Runtime.exn_message_list exn handle _ (*sic!*) => (build_session_finished ["CRASHED"]; raise Isabelle_Process.EXIT 2)); val _ = build_session_finished errs; in if null errs then raise Isabelle_Process.STOP else raise Isabelle_Process.EXIT 1 end | _ => raise Match); end;