# HG changeset patch # User paulson # Date 1605607057 0 # Node ID 20f70d20e6f8c86057ed90077837daa57da18d6f # Parent 5e616a454b230f253043008347ca33b5868002d9# Parent 773ad766f1b898f0c1b3dfa76f1e33c38816b060 merged diff -r 773ad766f1b8 -r 20f70d20e6f8 src/HOL/ROOT --- a/src/HOL/ROOT Tue Nov 17 09:57:25 2020 +0000 +++ b/src/HOL/ROOT Tue Nov 17 09:57:37 2020 +0000 @@ -9,6 +9,8 @@ theories Main (global) Complex_Main (global) + document_theories + Tools.Code_Generator document_files "root.bib" "root.tex" diff -r 773ad766f1b8 -r 20f70d20e6f8 src/HOL/document/root.tex --- a/src/HOL/document/root.tex Tue Nov 17 09:57:25 2020 +0000 +++ b/src/HOL/document/root.tex Tue Nov 17 09:57:37 2020 +0000 @@ -28,6 +28,7 @@ \renewcommand{\setisabellecontext}[1]{\markright{THEORY~``#1''}} \parindent 0pt\parskip 0.5ex +\input{Code_Generator.tex} \input{session} \pagestyle{headings} diff -r 773ad766f1b8 -r 20f70d20e6f8 src/Pure/ML/ml_console.scala --- a/src/Pure/ML/ml_console.scala Tue Nov 17 09:57:25 2020 +0000 +++ b/src/Pure/ML/ml_console.scala Tue Nov 17 09:57:37 2020 +0000 @@ -72,7 +72,7 @@ session_base = if (raw_ml_system) None else Some(Sessions.base_info( - options, logic, dirs = dirs, include_sessions = include_sessions).check_base)) + options, logic, dirs = dirs, include_sessions = include_sessions).check.base)) POSIX_Interrupt.handler { process.interrupt } { new TTY_Loop(process.stdin, process.stdout).join diff -r 773ad766f1b8 -r 20f70d20e6f8 src/Pure/ML/ml_process.scala --- a/src/Pure/ML/ml_process.scala Tue Nov 17 09:57:25 2020 +0000 +++ b/src/Pure/ML/ml_process.scala Tue Nov 17 09:57:37 2020 +0000 @@ -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) + @@ -197,11 +201,11 @@ val more_args = getopts(args) if (args.isEmpty || more_args.nonEmpty) getopts.usage() - val sessions_structure = Sessions.load_structure(options, dirs = dirs) + val base_info = Sessions.base_info(options, logic, dirs = dirs).check val store = Sessions.store(options) - val result = - ML_Process(options, sessions_structure, store, logic = logic, args = eval_args, modes = modes) + ML_Process(options, base_info.sessions_structure, store, logic = logic, args = eval_args, + modes = modes, session_base = Some(base_info.base)) .result( progress_stdout = Output.writeln(_, stdout = true), progress_stderr = Output.writeln(_)) diff -r 773ad766f1b8 -r 20f70d20e6f8 src/Pure/PIDE/headless.scala --- a/src/Pure/PIDE/headless.scala Tue Nov 17 09:57:25 2020 +0000 +++ b/src/Pure/PIDE/headless.scala Tue Nov 17 09:57:37 2020 +0000 @@ -558,7 +558,7 @@ val session_base_info: Sessions.Base_Info, log: Logger = No_Logger) extends isabelle.Resources( - session_base_info.sessions_structure, session_base_info.check_base, log = log) + session_base_info.sessions_structure, session_base_info.check.base, log = log) { resources => diff -r 773ad766f1b8 -r 20f70d20e6f8 src/Pure/PIDE/protocol.ML --- a/src/Pure/PIDE/protocol.ML Tue Nov 17 09:57:25 2020 +0000 +++ b/src/Pure/PIDE/protocol.ML Tue Nov 17 09:57:37 2020 +0000 @@ -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 773ad766f1b8 -r 20f70d20e6f8 src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Tue Nov 17 09:57:25 2020 +0000 +++ b/src/Pure/PIDE/protocol.scala Tue Nov 17 09:57:37 2020 +0000 @@ -289,6 +289,8 @@ { import XML.Encode._ + def encode_symbols(arg: List[(String, Int)]): String = + Symbol.encode_yxml(list(pair(string, int))(arg)) def encode_table(arg: List[(String, String)]): String = Symbol.encode_yxml(list(pair(string, string))(arg)) def encode_list(arg: List[String]): String = @@ -299,6 +301,7 @@ Symbol.encode_yxml(list(pair(string, list(string)))(arg)) protocol_command("Prover.init_session", + encode_symbols(Symbol.codes), encode_sessions(resources.sessions_structure.session_positions), encode_table(resources.sessions_structure.dest_session_directories), encode_table(resources.sessions_structure.session_chapters), diff -r 773ad766f1b8 -r 20f70d20e6f8 src/Pure/PIDE/resources.ML --- a/src/Pure/PIDE/resources.ML Tue Nov 17 09:57:25 2020 +0000 +++ b/src/Pure/PIDE/resources.ML Tue Nov 17 09:57:37 2020 +0000 @@ -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 773ad766f1b8 -r 20f70d20e6f8 src/Pure/PIDE/session.ML --- a/src/Pure/PIDE/session.ML Tue Nov 17 09:57:25 2020 +0000 +++ b/src/Pure/PIDE/session.ML Tue Nov 17 09:57:37 2020 +0000 @@ -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: string -> string * string -> unit val shutdown: unit -> unit val finish: unit -> unit end; @@ -45,12 +45,11 @@ (* init *) -fun init symbols info info_path documents parent (chapter, name) verbose = +fun init parent (chapter, name) = (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); + else ({chapter = chapter, name = name}, false))); (* finish *) @@ -64,7 +63,6 @@ (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))); diff -r 773ad766f1b8 -r 20f70d20e6f8 src/Pure/Thy/html.ML --- a/src/Pure/Thy/html.ML Tue Nov 17 09:57:25 2020 +0000 +++ b/src/Pure/Thy/html.ML Tue Nov 17 09:57:37 2020 +0000 @@ -1,5 +1,5 @@ (* Title: Pure/Thy/html.ML - Author: Markus Wenzel and Stefan Berghofer, TU Muenchen + Author: Makarius HTML presentation elements. *) @@ -11,11 +11,14 @@ val no_symbols: symbols val present_span: symbols -> Keyword.keywords -> Command_Span.span -> Output.output type text = string + val name: symbols -> string -> text + val keyword: symbols -> string -> text + val command: symbols -> string -> text + val href_name: string -> string -> string + val href_path: Url.T -> string -> string + val href_opt_path: Url.T option -> string -> string val begin_document: symbols -> string -> text val end_document: text - val begin_session_index: symbols -> string -> Url.T -> (Url.T * string) list -> text - val theory_entry: symbols -> Url.T * string -> text - val theory: symbols -> string -> (Url.T option * string) list -> text -> text end; structure HTML: HTML = @@ -120,8 +123,6 @@ fun href_opt_path NONE txt = txt | href_opt_path (SOME p) txt = href_path p txt; -fun para txt = "\n
" ^ txt ^ "
\n"; - (* document *) @@ -142,27 +143,4 @@ val end_document = "\n\n