diff --git a/src/Pure/PIDE/protocol_message.ML b/src/Pure/PIDE/protocol_message.ML --- a/src/Pure/PIDE/protocol_message.ML +++ b/src/Pure/PIDE/protocol_message.ML @@ -1,36 +1,36 @@ (* Title: Pure/PIDE/protocol_message.ML Author: Makarius Auxiliary operations on protocol messages. *) signature PROTOCOL_MESSAGE = sig - val inline_text: string -> string -> unit - val inline_properties: string -> Properties.T -> unit + val marker_text: string -> string -> unit + val marker: string -> Properties.T -> unit val command_positions: string -> XML.body -> XML.body val command_positions_yxml: string -> string -> string end; structure Protocol_Message: PROTOCOL_MESSAGE = struct -fun inline_text a text = +fun marker_text a text = Output.physical_writeln ("\f" ^ a ^ " = " ^ encode_lines text); -fun inline_properties a props = - inline_text a (YXML.string_of_body (XML.Encode.properties props)); +fun marker a props = + marker_text a (YXML.string_of_body (XML.Encode.properties props)); fun command_positions id = let fun attribute (a, b) = if a = Markup.idN andalso b = Markup.commandN then (a, id) else (a, b); fun tree (XML.Elem ((a, atts), ts)) = XML.Elem ((a, map attribute atts), map tree ts) | tree text = text; in map tree end; fun command_positions_yxml id = YXML.string_of_body o command_positions id o YXML.parse_body; end; diff --git a/src/Pure/Thy/export.ML b/src/Pure/Thy/export.ML --- a/src/Pure/Thy/export.ML +++ b/src/Pure/Thy/export.ML @@ -1,97 +1,94 @@ (* Title: Pure/Thy/export.ML Author: Makarius Manage theory exports: compressed blobs. *) signature EXPORT = sig val report_export: theory -> Path.binding -> unit type params = {theory: theory, binding: Path.binding, executable: bool, compress: bool, strict: bool} val export_params: params -> XML.body -> unit val export: theory -> Path.binding -> XML.body -> unit val export_executable: theory -> Path.binding -> XML.body -> unit val export_file: theory -> Path.binding -> Path.T -> unit val export_executable_file: theory -> Path.binding -> Path.T -> unit val markup: theory -> Path.T -> Markup.T val message: theory -> Path.T -> string val protocol_message: Output.protocol_message_fn end; structure Export: EXPORT = struct (* export *) fun report_export thy binding = let val theory_name = Context.theory_long_name thy; val (path, pos) = Path.dest_binding binding; val markup = Markup.export_path (Path.implode (Path.append (Path.basic theory_name) path)); in Context_Position.report_generic (Context.Theory thy) pos markup end; type params = {theory: theory, binding: Path.binding, executable: bool, compress: bool, strict: bool}; fun export_params ({theory = thy, binding, executable, compress, strict}: params) body = (report_export thy binding; (Output.try_protocol_message o Markup.export) {id = Position.get_id (Position.thread_data ()), serial = serial (), theory_name = Context.theory_long_name thy, name = Path.implode_binding (tap Path.proper_binding binding), executable = executable, compress = compress, strict = strict} body); fun export thy binding body = export_params {theory = thy, binding = binding, executable = false, compress = true, strict = true} body; fun export_executable thy binding body = export_params {theory = thy, binding = binding, executable = true, compress = true, strict = true} body; fun export_file thy binding file = export thy binding [XML.Text (File.read file)]; fun export_executable_file thy binding file = export_executable thy binding [XML.Text (File.read file)]; (* information message *) fun markup thy path = let val thy_path = Path.append (Path.basic (Context.theory_long_name thy)) path; val name = (Markup.nameN, Path.implode thy_path); in Active.make_markup Markup.theory_exportsN {implicit = false, properties = [name]} end; fun message thy path = "See " ^ Markup.markup (markup thy path) "theory exports"; (* protocol message (bootstrap) *) fun protocol_message props body = (case props of function :: args => if function = (Markup.functionN, Markup.exportN) andalso not (null args) andalso #1 (hd args) = Markup.idN then let val path = Path.expand (Path.explode ("$ISABELLE_EXPORT_TMP/export" ^ serial_string ())); val _ = YXML.write_body path body; - in - Protocol_Message.inline_properties (#2 function) - (tl args @ [(Markup.fileN, Path.implode path)]) - end + in Protocol_Message.marker (#2 function) (tl args @ [(Markup.fileN, Path.implode path)]) end else raise Output.Protocol_Message props | [] => raise Output.Protocol_Message props); val _ = if Thread_Data.is_virtual then () else Private_Output.protocol_message_fn := protocol_message; 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,254 +1,254 @@ (* 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 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.inline_properties "Timing" timing_props; + val _ = Protocol_Message.marker "Timing" timing_props; val _ = if verbose then Output.physical_stderr ("Timing " ^ 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.inline_properties (#2 function) args + 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.inline_properties (#2 function) + Protocol_Message.marker (#2 function) (Markup.command_timing_properties id elapsed) | NONE => ()) else () end else if function = Markup.theory_timing then - Protocol_Message.inline_properties (#2 function) args + Protocol_Message.marker (#2 function) args else (case Markup.dest_loading_theory props of - SOME name => Protocol_Message.inline_text "loading_theory" name + 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, 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, 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 = 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, (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, 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, name = 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, graph_file, parent_name, chapter, 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_base {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, 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 name master_dir) |> session_timing name verbose |> Exn.capture); val res2 = Exn.capture Session.finish (); val _ = Resources.finish_session_base (); val _ = Par_Exn.release_all [res1, res2]; val _ = if name = Context.PureN then Theory.install_pure (Thy_Info.get_theory Context.PureN) else (); in () end; fun inline_errors exn = Runtime.exn_message_list exn - |> List.app (fn msg => Protocol_Message.inline_text "error_message" (YXML.content_of msg)); + |> List.app (fn msg => Protocol_Message.marker_text "error_message" (YXML.content_of msg)); (*command-line tool*) 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 _ = 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*) val _ = Isabelle_Process.protocol_command "build_session" (fn [args_yxml] => let val args = decode_args args_yxml; val result = (build_session args; "") handle exn => (Runtime.exn_message exn handle _ (*sic!*) => "Exception raised, but failed to print details!"); in Output.protocol_message Markup.build_session_finished [XML.Text result] end | _ => raise Match); end;