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,211 +1,215 @@ /* 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(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 init_session = Isabelle_System.tmp_file("init_session", ext = "ML") val init_session_name = init_session.getAbsolutePath Isabelle_System.chmod("600", File.path(init_session)) File.write(init_session, session_base match { case None => "" case Some(base) => + def print_symbols: List[(String, Int)] => String = + ML_Syntax.print_list( + ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_int)) def print_table: List[(String, String)] => String = ML_Syntax.print_list( ML_Syntax.print_pair( ML_Syntax.print_string_bytes, ML_Syntax.print_string_bytes)) def print_list: List[String] => String = ML_Syntax.print_list(ML_Syntax.print_string_bytes) def print_sessions: List[(String, Position.T)] => String = ML_Syntax.print_list( ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_properties)) def print_bibtex_entries: List[(String, List[String])] => String = ML_Syntax.print_list( ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_list(ML_Syntax.print_string_bytes))) "Resources.init_session" + - "{session_positions = " + print_sessions(sessions_structure.session_positions) + + "{html_symbols = " + print_symbols(Symbol.codes) + + ", session_positions = " + print_sessions(sessions_structure.session_positions) + ", session_directories = " + print_table(sessions_structure.dest_session_directories) + ", session_chapters = " + print_table(sessions_structure.session_chapters) + ", bibtex_entries = " + print_bibtex_entries(sessions_structure.bibtex_entries) + ", 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), "POLYSTATSDIR" -> isabelle_tmp.getAbsolutePath) val env_functions = Map("ISABELLE_SCALA_FUNCTIONS" -> Scala.functions.mkString(",")) 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 ::: List("--exportstats") } // bash val bash_args = ml_runtime_options ::: (eval_init ::: eval_modes ::: eval_options).flatMap(List("--eval", _)) ::: List("--use", init_session_name, "--eval", "OS.FileSys.remove " + ML_Syntax.print_string_bytes(init_session_name)) ::: 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 ++ env_functions, redirect = redirect, cleanup = () => { isabelle_process_options.delete init_session.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 result = ML_Process(options, sessions_structure, store, logic = logic, args = eval_args, modes = modes) .result( progress_stdout = Output.writeln(_, stdout = true), progress_stderr = Output.writeln(_)) sys.exit(result.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,188 +1,190 @@ (* 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.stop" (fn rc :: msgs => (List.app Output.system_message msgs; raise Isabelle_Process.STOP (Value.parse_int rc))); 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, session_chapters_yxml, + (fn [html_symbols_yxml, session_positions_yxml, session_directories_yxml, session_chapters_yxml, bibtex_entries_yxml, doc_names_yxml, global_theories_yxml, loaded_theories_yxml] => let + val decode_symbols = YXML.parse_body #> let open XML.Decode in list (pair string int) end; 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; val decode_bibtex_entries = YXML.parse_body #> let open XML.Decode in list (pair string (list string)) end; in Resources.init_session - {session_positions = decode_sessions session_positions_yxml, + {html_symbols = decode_symbols html_symbols_yxml, + session_positions = decode_sessions session_positions_yxml, session_directories = decode_table session_directories_yxml, session_chapters = decode_table session_chapters_yxml, bibtex_entries = decode_bibtex_entries bibtex_entries_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.full_gc" (fn [] => ML_Heap.full_gc ()); 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,324 +1,330 @@ (* 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, + {html_symbols: (string * int) list, + session_positions: (string * Properties.T) list, session_directories: (string * string) list, session_chapters: (string * string) list, bibtex_entries: (string * string list) list, docs: string list, global_theories: (string * string) list, loaded_theories: string list} -> unit val finish_session_base: unit -> unit val global_theory: string -> string option val loaded_theory: string -> bool + val html_symbols: unit -> HTML.symbols val check_session: Proof.context -> string * Position.T -> string val session_chapter: string -> 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 theory_bibtex_entries: string -> string list 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, + {html_symbols = HTML.no_symbols, + session_positions = []: (string * entry) list, session_directories = Symtab.empty: Path.T list Symtab.table, session_chapters = Symtab.empty: string Symtab.table, bibtex_entries = Symtab.empty: string 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, session_chapters, + {html_symbols, session_positions, session_directories, session_chapters, bibtex_entries, docs, global_theories, loaded_theories} = Synchronized.change global_session_base (fn _ => - {session_positions = sort_by #1 (map (apsnd make_entry) session_positions), + {html_symbols = HTML.make_symbols html_symbols, + 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, session_chapters = Symtab.make session_chapters, bibtex_entries = Symtab.make bibtex_entries, 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 = [], + {html_symbols = HTML.no_symbols, + session_positions = [], session_directories = Symtab.empty, session_chapters = Symtab.empty, bibtex_entries = Symtab.empty, docs = [], global_theories = global_theories, loaded_theories = loaded_theories}); fun get_session_base f = f (Synchronized.value global_session_base); 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 html_symbols () = get_session_base #html_symbols; fun check_name which kind markup ctxt arg = Completion.check_item kind markup (get_session_base which |> sort_by #1) ctxt arg; val check_session = check_name #session_positions "session" (fn (name, {pos, serial}) => Markup.entity Markup.sessionN name |> Markup.properties (Position.entity_properties_of false serial pos)); fun session_chapter name = the_default "Unsorted" (Symtab.lookup (get_session_base #session_chapters) name); val check_doc = check_name #docs "documentation" (Markup.doc o #1); (* 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, [], []); val extend = I; fun merge ({master_dir, imports, provided = provided1}, {provided = provided2, ...}) = let val provided' = Library.merge (op =) (provided1, provided2) in make_files (master_dir, imports, provided') end ); 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.implode_symbolic 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 theory_bibtex_entries theory = Symtab.lookup_list (get_session_base #bibtex_entries) (theory_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 = 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 = 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.implode_symbolic 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 = Latex.string (Latex.output_ascii_breakable "/" name); in Latex.enclose_block "\\isatt{" "}" [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/PIDE/session.ML b/src/Pure/PIDE/session.ML --- a/src/Pure/PIDE/session.ML +++ b/src/Pure/PIDE/session.ML @@ -1,72 +1,72 @@ (* Title: Pure/PIDE/session.ML Author: Makarius Prover session: persistent state of logic image. *) signature SESSION = sig val get_name: unit -> string val welcome: unit -> string val get_keywords: unit -> Keyword.keywords - val init: HTML.symbols -> bool -> Path.T -> string list -> string -> string * string -> bool -> unit + val init: bool -> Path.T -> string list -> string -> string * string -> bool -> unit val shutdown: unit -> unit val finish: unit -> unit end; structure Session: SESSION = struct (** persistent session information **) val session = Synchronized.var "Session.session" ({chapter = "", name = ""}, true); fun get_name () = #name (#1 (Synchronized.value session)); fun description () = "Isabelle/" ^ get_name (); fun welcome () = if Distribution.is_identified then "Welcome to " ^ description () ^ " (" ^ Distribution.version ^ ")" else "Unofficial version of " ^ description () ^ " (" ^ Distribution.version ^ ")"; (* base syntax *) val keywords = Synchronized.var "Session.keywords" Keyword.empty_keywords; fun get_keywords () = Synchronized.value keywords; fun update_keywords () = Synchronized.change keywords (K (fold (curry Keyword.merge_keywords o Thy_Header.get_keywords o Thy_Info.get_theory) (Thy_Info.get_names ()) Keyword.empty_keywords)); (* init *) -fun init symbols info info_path documents parent (chapter, name) verbose = +fun init info info_path documents parent (chapter, name) verbose = (Synchronized.change session (fn ({name = parent_name, ...}, parent_finished) => if parent_name <> parent orelse not parent_finished then error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name) else ({chapter = chapter, name = name}, false)); - Present.init symbols info info_path documents (chapter, name) verbose); + Present.init info info_path documents (chapter, name) verbose); (* finish *) fun shutdown () = (Execution.shutdown (); Event_Timer.shutdown (); Future.shutdown ()); fun finish () = (shutdown (); Par_List.map (Global_Theory.get_thm_names o Thy_Info.get_theory) (Thy_Info.get_names ()); Thy_Info.finish (); Present.finish (); shutdown (); update_keywords (); Synchronized.change session (apsnd (K true))); end; diff --git a/src/Pure/Thy/present.ML b/src/Pure/Thy/present.ML --- a/src/Pure/Thy/present.ML +++ b/src/Pure/Thy/present.ML @@ -1,169 +1,168 @@ (* Title: Pure/Thy/present.ML Author: Markus Wenzel and Stefan Berghofer, TU Muenchen Theory presentation: HTML and PDF-LaTeX documents. *) signature PRESENT = sig - val init: HTML.symbols -> bool -> Path.T -> string list -> string * string -> bool -> unit + val init: bool -> Path.T -> string list -> string * string -> bool -> unit val finish: unit -> unit - val begin_theory: int -> (unit -> HTML.text) -> theory -> theory + val begin_theory: int -> HTML.text -> theory -> theory end; structure Present: PRESENT = struct (** paths **) val html_ext = Path.ext "html"; val html_path = html_ext o Path.basic; val index_path = Path.basic "index.html"; val readme_html_path = Path.basic "README.html"; val session_graph_path = Path.basic "session_graph.pdf"; val document_path = Path.ext "pdf" o Path.basic; fun show_path path = Path.implode (Path.expand (File.full_path Path.current path)); (** global browser info state **) (* type browser_info *) type browser_info = {html_theories: string Symtab.table, html_index: (int * string) list}; fun make_browser_info (html_theories, html_index) : browser_info = {html_theories = html_theories, html_index = html_index}; val empty_browser_info = make_browser_info (Symtab.empty, []); fun map_browser_info f {html_theories, html_index} = make_browser_info (f (html_theories, html_index)); (* state *) val browser_info = Synchronized.var "browser_info" empty_browser_info; fun change_browser_info f = Synchronized.change browser_info (map_browser_info f); fun update_html name html = change_browser_info (apfst (Symtab.update (name, html))); fun add_html_index txt = change_browser_info (apsnd (cons txt)); (** global session state **) (* session_info *) type session_info = - {symbols: HTML.symbols, name: string, chapter: string, info_path: Path.T, info: bool, + {name: string, chapter: string, info_path: Path.T, info: bool, verbose: bool, readme: Path.T option}; -fun make_session_info - (symbols, name, chapter, info_path, info, verbose, readme) = - {symbols = symbols, name = name, chapter = chapter, info_path = info_path, info = info, +fun make_session_info (name, chapter, info_path, info, verbose, readme) = + {name = name, chapter = chapter, info_path = info_path, info = info, verbose = verbose, readme = readme}: session_info; (* state *) val session_info = Unsynchronized.ref (NONE: session_info option); fun with_session_info x f = (case ! session_info of NONE => x | SOME info => f info); val theory_qualifier = Resources.theory_qualifier o Context.theory_long_name; fun is_session_theory thy = (case ! session_info of NONE => false | SOME {name, ...} => name = theory_qualifier thy); (** document preparation **) (* init session *) -fun init symbols info info_path documents (chapter, name) verbose = +fun init info info_path documents (chapter, name) verbose = let val readme = if File.exists readme_html_path then SOME readme_html_path else NONE; - + val symbols = Resources.html_symbols (); val docs = (case readme of NONE => [] | SOME p => [(Url.File p, "README")]) @ map (fn name => (Url.File (document_path name), name)) documents; in - session_info := - SOME (make_session_info (symbols, name, chapter, info_path, info, verbose, readme)); + session_info := SOME (make_session_info (name, chapter, info_path, info, verbose, readme)); Synchronized.change browser_info (K empty_browser_info); add_html_index (0, HTML.begin_session_index symbols name (Url.File session_graph_path) docs) end; (* finish session -- output all generated text *) fun sorted_index index = map snd (sort (int_ord o apply2 fst) (rev index)); fun index_buffer index = Buffer.add (implode (sorted_index index)) Buffer.empty; fun finish () = with_session_info () (fn {name, chapter, info, info_path, verbose, readme, ...} => let val {html_theories, html_index} = Synchronized.value browser_info; val session_prefix = info_path + Path.basic chapter + Path.basic name; fun finish_html (a, html) = File.write (session_prefix + html_path a) html; val _ = if info then (Isabelle_System.make_directory session_prefix; File.write_buffer (session_prefix + index_path) (index_buffer html_index |> Buffer.add HTML.end_document); (case readme of NONE => () | SOME path => Isabelle_System.copy_file path session_prefix); Symtab.fold (K o finish_html) html_theories (); if verbose then Output.physical_stderr ("Browser info at " ^ show_path session_prefix ^ "\n") else ()) else (); in Synchronized.change browser_info (K empty_browser_info); session_info := NONE end); (* theory elements *) fun theory_link (curr_chapter, curr_session) thy = let val session = Resources.theory_qualifier (Context.theory_long_name thy); val chapter = Resources.session_chapter session; val link = html_path (Context.theory_name thy); in if curr_session = session then SOME link else if curr_chapter = chapter then SOME (Path.parent + Path.basic session + link) else if chapter = Context.PureN then NONE else SOME (Path.parent + Path.parent + Path.basic chapter + Path.basic session + link) end; -fun begin_theory update_time mk_text thy = - with_session_info thy (fn {symbols, name = session_name, chapter, ...} => +fun begin_theory update_time html thy = + with_session_info thy (fn {name = session_name, chapter, ...} => let val name = Context.theory_name thy; val parent_specs = Theory.parents_of thy |> map (fn parent => (Option.map Url.File (theory_link (chapter, session_name) parent), (Context.theory_name parent))); - val _ = update_html name (HTML.theory symbols name parent_specs (mk_text ())); + val symbols = Resources.html_symbols (); + val _ = update_html name (HTML.theory symbols name parent_specs html); val _ = if is_session_theory thy then add_html_index (update_time, HTML.theory_entry symbols (Url.File (html_path name), name)) else (); in thy end); end; diff --git a/src/Pure/Thy/thy_info.ML b/src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML +++ b/src/Pure/Thy/thy_info.ML @@ -1,482 +1,477 @@ (* Title: Pure/Thy/thy_info.ML Author: Markus Wenzel, TU Muenchen Global theory info database, with auto-loading according to theory and file dependencies. *) signature THY_INFO = sig type presentation_context = {options: Options.T, file_pos: Position.T, adjust_pos: Position.T -> Position.T, segments: Thy_Output.segment list} val adjust_pos_properties: presentation_context -> Position.T -> Properties.T val apply_presentation: presentation_context -> theory -> unit val add_presentation: (presentation_context -> theory -> unit) -> theory -> theory val get_names: unit -> string list val lookup_theory: string -> theory option val get_theory: string -> theory val master_directory: string -> Path.T val remove_thy: string -> unit - type context = - {options: Options.T, - symbols: HTML.symbols, - last_timing: Toplevel.transition -> Time.time} + type context = {options: Options.T, last_timing: Toplevel.transition -> Time.time} val use_theories: context -> string -> Path.T -> (string * Position.T) list -> unit val use_thy: string -> unit val script_thy: Position.T -> string -> theory -> theory val register_thy: theory -> unit val finish: unit -> unit end; structure Thy_Info: THY_INFO = struct (** presentation of consolidated theory **) type presentation_context = {options: Options.T, file_pos: Position.T, adjust_pos: Position.T -> Position.T, segments: Thy_Output.segment list}; fun adjust_pos_properties (context: presentation_context) pos = Position.offset_properties_of (#adjust_pos context pos) @ Position.id_properties_of pos; structure Presentation = Theory_Data ( type T = ((presentation_context -> theory -> unit) * stamp) list; val empty = []; val extend = I; fun merge data : T = Library.merge (eq_snd op =) data; ); fun apply_presentation (context: presentation_context) thy = ignore (Presentation.get thy |> Par_List.map (fn (f, _) => f context thy)); fun add_presentation f = Presentation.map (cons (f, stamp ())); val _ = Theory.setup (add_presentation (fn {options, file_pos, segments, ...} => fn thy => if exists (Toplevel.is_skipped_proof o #state) segments then () else let val body = Thy_Output.present_thy options thy segments; in if Options.string options "document" = "false" then () else let val thy_name = Context.theory_name thy; val document_tex_name = Path.explode_binding0 ("document/" ^ thy_name ^ ".tex"); + val latex = Latex.isabelle_body thy_name body; val output = [Latex.output_text latex, Latex.output_positions file_pos latex]; in Export.export thy document_tex_name (XML.blob output) end end)); (** thy database **) (* messages *) val show_path = space_implode " via " o map quote; fun cycle_msg names = "Cyclic dependency of " ^ show_path names; (* derived graph operations *) fun add_deps name parents G = String_Graph.add_deps_acyclic (name, parents) G handle String_Graph.CYCLES namess => error (cat_lines (map cycle_msg namess)); fun new_entry name parents entry = String_Graph.new_node (name, entry) #> add_deps name parents; (* global thys *) type deps = {master: (Path.T * SHA1.digest), (*master dependencies for thy file*) imports: (string * Position.T) list}; (*source specification of imports (partially qualified)*) fun make_deps master imports : deps = {master = master, imports = imports}; fun master_dir_deps (d: deps option) = the_default Path.current (Option.map (Path.dir o #1 o #master) d); local val global_thys = Synchronized.var "Thy_Info.thys" (String_Graph.empty: (deps option * theory option) String_Graph.T); in fun get_thys () = Synchronized.value global_thys; fun change_thys f = Synchronized.change global_thys f; end; fun get_names () = String_Graph.topological_order (get_thys ()); (* access thy *) fun lookup thys name = try (String_Graph.get_node thys) name; fun lookup_thy name = lookup (get_thys ()) name; fun get thys name = (case lookup thys name of SOME thy => thy | NONE => error ("Theory loader: nothing known about theory " ^ quote name)); fun get_thy name = get (get_thys ()) name; (* access deps *) val lookup_deps = Option.map #1 o lookup_thy; val master_directory = master_dir_deps o #1 o get_thy; (* access theory *) fun lookup_theory name = (case lookup_thy name of SOME (_, SOME theory) => SOME theory | _ => NONE); fun get_theory name = (case lookup_theory name of SOME theory => theory | _ => error ("Theory loader: undefined entry for theory " ^ quote name)); val get_imports = Resources.imports_of o get_theory; (** thy operations **) (* remove *) fun remove name thys = (case lookup thys name of NONE => thys | SOME (NONE, _) => error ("Cannot update finished theory " ^ quote name) | SOME _ => let val succs = String_Graph.all_succs thys [name]; val _ = writeln ("Theory loader: removing " ^ commas_quote succs); in fold String_Graph.del_node succs thys end); val remove_thy = change_thys o remove; (* update *) fun update deps theory thys = let val name = Context.theory_long_name theory; val parents = map Context.theory_long_name (Theory.parents_of theory); val thys' = remove name thys; val _ = map (get thys') parents; in new_entry name parents (SOME deps, SOME theory) thys' end; fun update_thy deps theory = change_thys (update deps theory); (* context *) -type context = - {options: Options.T, - symbols: HTML.symbols, - last_timing: Toplevel.transition -> Time.time}; +type context = {options: Options.T, last_timing: Toplevel.transition -> Time.time}; fun default_context (): context = - {options = Options.default (), - symbols = HTML.no_symbols, - last_timing = K Time.zeroTime}; + {options = Options.default (), last_timing = K Time.zeroTime}; (* scheduling loader tasks *) datatype result = Result of {theory: theory, exec_id: Document_ID.exec, present: unit -> unit, commit: unit -> unit, weight: int}; fun theory_result theory = Result {theory = theory, exec_id = Document_ID.none, present = I, commit = I, weight = 0}; fun result_theory (Result {theory, ...}) = theory; fun result_present (Result {present, ...}) = present; fun result_commit (Result {commit, ...}) = commit; fun result_ord (Result {weight = i, ...}, Result {weight = j, ...}) = int_ord (j, i); fun join_theory (Result {theory, exec_id, ...}) = let val _ = Execution.join [exec_id]; val res = Exn.capture Thm.consolidate_theory theory; val exns = maps Task_Queue.group_status (Execution.peek exec_id); in res :: map Exn.Exn exns end; datatype task = Task of string list * (theory list -> result) | Finished of theory; fun task_finished (Task _) = false | task_finished (Finished _) = true; fun task_parents deps (parents: string list) = map (the o AList.lookup (op =) deps) parents; val schedule_seq = String_Graph.schedule (fn deps => fn (_, task) => (case task of Task (parents, body) => let val result = body (task_parents deps parents); val _ = Par_Exn.release_all (join_theory result); val _ = result_present result (); val _ = result_commit result (); in result_theory result end | Finished thy => thy)) #> ignore; val schedule_futures = Thread_Attributes.uninterruptible (fn _ => fn tasks => let val futures = tasks |> String_Graph.schedule (fn deps => fn (name, task) => (case task of Task (parents, body) => (singleton o Future.forks) {name = "theory:" ^ name, group = NONE, deps = map (Future.task_of o #2) deps, pri = 0, interrupts = true} (fn () => (case filter (not o can Future.join o #2) deps of [] => body (map (result_theory o Future.join) (task_parents deps parents)) | bad => error ("Failed to load theory " ^ quote name ^ " (unresolved " ^ commas_quote (map #1 bad) ^ ")"))) | Finished theory => Future.value (theory_result theory))); val results1 = futures |> maps (fn future => (case Future.join_result future of Exn.Res result => join_theory result | Exn.Exn exn => [Exn.Exn exn])); val results2 = futures |> map_filter (Exn.get_res o Future.join_result) |> sort result_ord |> Par_List.map (fn result => Exn.capture (result_present result) ()); (* FIXME more precise commit order (!?) *) val results3 = futures |> map (fn future => Exn.capture (fn () => result_commit (Future.join future) ()) ()); (* FIXME avoid global Execution.reset (!??) *) val results4 = map Exn.Exn (maps Task_Queue.group_status (Execution.reset ())); val _ = Par_Exn.release_all (results1 @ results2 @ results3 @ results4); in () end); (* eval theory *) fun excursion keywords master_dir last_timing init elements = let fun prepare_span st span = Command_Span.content span |> Command.read keywords (Command.read_thy st) master_dir init ([], ~1) |> (fn tr => Toplevel.timing (last_timing tr) tr); fun element_result span_elem (st, _) = let val elem = Thy_Element.map_element (prepare_span st) span_elem; val (results, st') = Toplevel.element_result keywords elem st; val pos' = Toplevel.pos_of (Thy_Element.last_element elem); in (results, (st', pos')) end; val (results, (end_state, end_pos)) = fold_map element_result elements (Toplevel.init_toplevel (), Position.none); val thy = Toplevel.end_theory end_pos end_state; in (results, thy) end; fun eval_thy (context: context) update_time master_dir header text_pos text parents = let - val {options, symbols, last_timing} = context; + val {options, last_timing} = context; val (name, _) = #name header; val keywords = fold (curry Keyword.merge_keywords o Thy_Header.get_keywords) parents (Keyword.add_keywords (#keywords header) Keyword.empty_keywords); val spans = Outer_Syntax.parse_spans (Token.explode keywords text_pos text); val elements = Thy_Element.parse_elements keywords spans; + val symbols = Resources.html_symbols (); + val html = implode (map (HTML.present_span symbols keywords) spans); + fun init () = Resources.begin_theory master_dir header parents - |> Present.begin_theory update_time - (fn () => implode (map (HTML.present_span symbols keywords) spans)); + |> Present.begin_theory update_time html; val (results, thy) = cond_timeit true ("theory " ^ quote name) (fn () => excursion keywords master_dir last_timing init elements); fun present () = let val segments = (spans ~~ maps Toplevel.join_results results) |> map (fn (span, (tr, st')) => {span = span, command = tr, state = st'}); val context: presentation_context = {options = options, file_pos = text_pos, adjust_pos = I, segments = segments}; in apply_presentation context thy end; in (thy, present, size text) end; (* require_thy -- checking database entries wrt. the file-system *) local fun required_by _ [] = "" | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")"; fun load_thy context initiators update_time deps text (name, pos) keywords parents = let val _ = remove_thy name; val _ = writeln ("Loading theory " ^ quote name ^ required_by " " initiators); val _ = Output.try_protocol_message (Markup.loading_theory name) []; val {master = (thy_path, _), imports} = deps; val dir = Path.dir thy_path; val header = Thy_Header.make (name, pos) imports keywords; val _ = (imports ~~ parents) |> List.app (fn ((_, pos), thy) => Context_Position.reports_global thy [(pos, Theory.get_markup thy)]); val exec_id = Document_ID.make (); val _ = Execution.running Document_ID.none exec_id [] orelse raise Fail ("Failed to register execution: " ^ Document_ID.print exec_id); val timing_start = Timing.start (); val text_pos = Position.put_id (Document_ID.print exec_id) (Path.position thy_path); val (theory, present, weight) = eval_thy context update_time dir header text_pos text (if name = Context.PureN then [Context.the_global_context ()] else parents); val timing_result = Timing.result timing_start; val timing_props = [Markup.theory_timing, (Markup.nameN, name)]; val _ = Output.try_protocol_message (timing_props @ Markup.timing_properties timing_result) [] fun commit () = update_thy deps theory; in Result {theory = theory, exec_id = exec_id, present = present, commit = commit, weight = weight} end; fun check_thy_deps dir name = (case lookup_deps name of SOME NONE => (true, NONE, Position.none, get_imports name, []) | NONE => let val {master, text, theory_pos, imports, keywords} = Resources.check_thy dir name in (false, SOME (make_deps master imports, text), theory_pos, imports, keywords) end | SOME (SOME {master, ...}) => let val {master = master', text = text', theory_pos = theory_pos', imports = imports', keywords = keywords'} = Resources.check_thy dir name; val deps' = SOME (make_deps master' imports', text'); val current = #2 master = #2 master' andalso (case lookup_theory name of NONE => false | SOME theory => Resources.loaded_files_current theory); in (current, deps', theory_pos', imports', keywords') end); in fun require_thys context initiators qualifier dir strs tasks = fold_map (require_thy context initiators qualifier dir) strs tasks |>> forall I and require_thy context initiators qualifier dir (s, require_pos) tasks = let val {master_dir, theory_name, ...} = Resources.import_name qualifier dir s; in (case try (String_Graph.get_node tasks) theory_name of SOME task => (task_finished task, tasks) | NONE => let val _ = member (op =) initiators theory_name andalso error (cycle_msg initiators); val (current, deps, theory_pos, imports, keywords) = check_thy_deps master_dir theory_name handle ERROR msg => cat_error msg ("The error(s) above occurred for theory " ^ quote theory_name ^ Position.here require_pos ^ required_by "\n" initiators); val qualifier' = Resources.theory_qualifier theory_name; val dir' = dir + master_dir_deps (Option.map #1 deps); val parents = map (#theory_name o Resources.import_name qualifier' dir' o #1) imports; val (parents_current, tasks') = require_thys context (theory_name :: initiators) qualifier' dir' imports tasks; val all_current = current andalso parents_current; val task = if all_current then Finished (get_theory theory_name) else (case deps of NONE => raise Fail "Malformed deps" | SOME (dep, text) => let val update_time = serial (); val load = load_thy context initiators update_time dep text (theory_name, theory_pos) keywords; in Task (parents, load) end); val tasks'' = new_entry theory_name parents task tasks'; in (all_current, tasks'') end) end; end; (* use theories *) fun use_theories context qualifier master_dir imports = let val (_, tasks) = require_thys context [] qualifier master_dir imports String_Graph.empty in if Multithreading.max_threads () > 1 then schedule_futures tasks else schedule_seq tasks end; fun use_thy name = use_theories (default_context ()) Resources.default_qualifier Path.current [(name, Position.none)]; (* toplevel scripting -- without maintaining database *) fun script_thy pos txt thy = let val trs = Outer_Syntax.parse_text thy (K thy) pos txt; val end_pos = if null trs then pos else Toplevel.pos_of (List.last trs); val end_state = fold (Toplevel.command_exception true) trs (Toplevel.init_toplevel ()); in Toplevel.end_theory end_pos end_state end; (* register theory *) fun register_thy theory = let val name = Context.theory_long_name theory; val {master, ...} = Resources.check_thy (Resources.master_directory theory) name; val imports = Resources.imports_of theory; in change_thys (fn thys => let val thys' = remove name thys; val _ = writeln ("Registering theory " ^ quote name); in update (make_deps master imports) theory thys' end) end; (* finish all theories *) fun finish () = change_thys (String_Graph.map (fn _ => fn (_, entry) => (NONE, entry))); end; fun use_thy name = Runtime.toplevel_program (fn () => Thy_Info.use_thy name); 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,167 +1,164 @@ (* Title: Pure/Tools/build.ML Author: Makarius Build Isabelle sessions. *) structure Build: sig end = 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 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 props = [("threads", threads)] @ Markup.timing_properties timing; val _ = Output.protocol_message (Markup.session_timing :: props) []; in y end; (* build theories *) -fun build_theories symbols last_timing qualifier master_dir (options, thys) = +fun build_theories last_timing qualifier master_dir (options, thys) = let - val context = - {options = options, symbols = symbols, last_timing = last_timing}; + val context = {options = options, 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 *) val _ = Isabelle_Process.protocol_command "build_session" (fn [args_yxml] => let - val (symbol_codes, (command_timings, (verbose, (browser_info, + val (html_symbols, (command_timings, (verbose, (browser_info, (documents, (parent_name, (chapter, (session_name, (master_dir, (theories, (session_positions, (session_directories, (session_chapters, (doc_names, (global_theories, (loaded_theories, bibtex_entries)))))))))))))))) = YXML.parse_body args_yxml |> let open XML.Decode; val position = Position.of_properties o properties; val path = Path.explode o string; in pair (list (pair string int)) (pair (list properties) (pair bool (pair path (pair (list string) (pair string (pair string (pair string (pair path (pair (((list (pair Options.decode (list (pair string position)))))) (pair (list (pair string properties)) (pair (list (pair string string)) (pair (list (pair string string)) (pair (list string) (pair (list (pair string string)) (pair (list string) (list (pair string (list string)))))))))))))))))) end; - val symbols = HTML.make_symbols symbol_codes; - fun build () = let val _ = Resources.init_session - {session_positions = session_positions, + {html_symbols = html_symbols, + session_positions = session_positions, session_directories = session_directories, session_chapters = session_chapters, bibtex_entries = bibtex_entries, docs = doc_names, global_theories = global_theories, loaded_theories = loaded_theories}; val _ = Session.init - symbols (Options.default_bool "browser_info") browser_info documents 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 last_timing session_name master_dir) + (List.app (build_theories last_timing session_name master_dir) |> session_timing |> 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; fun exec e = if can Theory.get_pure () then Isabelle_Thread.fork {name = "build_session", stack_limit = Isabelle_Thread.stack_limit (), interrupts = false} e |> ignore else e (); in exec (fn () => (Future.interruptible_task (fn () => (build (); (0, []))) () handle exn => ((1, Runtime.exn_message_list exn) handle _ (*sic!*) => (2, ["CRASHED"]))) |> let open XML.Encode in pair int (list string) end |> Output.protocol_message Markup.build_session_finished) end | _ => raise Match); end;