# HG changeset patch # User wenzelm # Date 1605528675 -3600 # Node ID 429afd0d1a799db76badb82b6dd7c187ca92be42 # Parent 4b2691211719d15aecc951732056386cedada784 refer to HTML symbols via resources; diff -r 4b2691211719 -r 429afd0d1a79 src/Pure/ML/ml_process.scala --- a/src/Pure/ML/ml_process.scala Sun Nov 15 16:51:58 2020 +0000 +++ b/src/Pure/ML/ml_process.scala Mon Nov 16 13:11:15 2020 +0100 @@ -85,6 +85,9 @@ 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( @@ -100,7 +103,8 @@ 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) + diff -r 4b2691211719 -r 429afd0d1a79 src/Pure/PIDE/protocol.ML --- a/src/Pure/PIDE/protocol.ML Sun Nov 15 16:51:58 2020 +0000 +++ b/src/Pure/PIDE/protocol.ML Mon Nov 16 13:11:15 2020 +0100 @@ -25,9 +25,10 @@ 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 = @@ -36,7 +37,8 @@ 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, diff -r 4b2691211719 -r 429afd0d1a79 src/Pure/PIDE/resources.ML --- a/src/Pure/PIDE/resources.ML Sun Nov 15 16:51:58 2020 +0000 +++ b/src/Pure/PIDE/resources.ML Mon Nov 16 13:11:15 2020 +0100 @@ -8,7 +8,8 @@ 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, @@ -18,6 +19,7 @@ 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 @@ -56,7 +58,8 @@ {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, @@ -68,11 +71,12 @@ 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, @@ -85,7 +89,8 @@ 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, @@ -98,6 +103,7 @@ 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; diff -r 4b2691211719 -r 429afd0d1a79 src/Pure/PIDE/session.ML --- a/src/Pure/PIDE/session.ML Sun Nov 15 16:51:58 2020 +0000 +++ b/src/Pure/PIDE/session.ML Mon Nov 16 13:11:15 2020 +0100 @@ -9,7 +9,7 @@ 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; @@ -45,12 +45,12 @@ (* 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 *) diff -r 4b2691211719 -r 429afd0d1a79 src/Pure/Thy/present.ML --- a/src/Pure/Thy/present.ML Sun Nov 15 16:51:58 2020 +0000 +++ b/src/Pure/Thy/present.ML Mon Nov 16 13:11:15 2020 +0100 @@ -6,9 +6,9 @@ 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 = @@ -61,12 +61,11 @@ (* 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; @@ -88,16 +87,15 @@ (* 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; @@ -148,8 +146,8 @@ 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; @@ -158,7 +156,8 @@ (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 diff -r 4b2691211719 -r 429afd0d1a79 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Sun Nov 15 16:51:58 2020 +0000 +++ b/src/Pure/Thy/thy_info.ML Mon Nov 16 13:11:15 2020 +0100 @@ -18,10 +18,7 @@ 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 @@ -66,6 +63,7 @@ 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 @@ -183,15 +181,10 @@ (* 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 *) @@ -300,7 +293,7 @@ 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 @@ -309,10 +302,12 @@ 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) diff -r 4b2691211719 -r 429afd0d1a79 src/Pure/Tools/build.ML --- a/src/Pure/Tools/build.ML Sun Nov 15 16:51:58 2020 +0000 +++ b/src/Pure/Tools/build.ML Mon Nov 16 13:11:15 2020 +0100 @@ -55,10 +55,9 @@ (* 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 @@ -87,7 +86,7 @@ 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)))))))))))))))) = @@ -108,13 +107,12 @@ (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, @@ -124,7 +122,6 @@ val _ = Session.init - symbols (Options.default_bool "browser_info") browser_info documents @@ -136,7 +133,7 @@ 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 ();