# HG changeset patch # User wenzelm # Date 1516370146 -3600 # Node ID bddfa23a4ea96040c2a025148ce1f1d7fb04c693 # Parent d36fcde7e2c012d56be4e62b800f9f2c9eb20d50 formal treatment of documentation names; diff -r d36fcde7e2c0 -r bddfa23a4ea9 src/Pure/ML/ml_process.scala --- a/src/Pure/ML/ml_process.scala Fri Jan 19 14:55:00 2018 +0100 +++ b/src/Pure/ML/ml_process.scala Fri Jan 19 14:55:46 2018 +0100 @@ -103,6 +103,7 @@ ML_Syntax.print_list(ML_Syntax.print_string_bytes)(list) List("Resources.init_session_base" + " {sessions = " + print_list(base.known.sessions.toList) + + ", doc_names = " + print_list(base.doc_names) + ", global_theories = " + print_table(base.global_theories.toList) + ", loaded_theories = " + print_list(base.loaded_theories.keys) + ", known_theories = " + print_table(base.dest_known_theories) + "}") diff -r d36fcde7e2c0 -r bddfa23a4ea9 src/Pure/PIDE/protocol.ML --- a/src/Pure/PIDE/protocol.ML Fri Jan 19 14:55:00 2018 +0100 +++ b/src/Pure/PIDE/protocol.ML Fri Jan 19 14:55:46 2018 +0100 @@ -19,13 +19,15 @@ val _ = Isabelle_Process.protocol_command "Prover.init_session_base" - (fn [sessions_yxml, global_theories_yxml, loaded_theories_yxml, known_theories_yxml] => + (fn [sessions_yxml, doc_names_yxml, global_theories_yxml, loaded_theories_yxml, + known_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; in Resources.init_session_base {sessions = decode_list sessions_yxml, + doc_names = decode_list doc_names_yxml, global_theories = decode_table global_theories_yxml, loaded_theories = decode_list loaded_theories_yxml, known_theories = decode_table known_theories_yxml} diff -r d36fcde7e2c0 -r bddfa23a4ea9 src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Fri Jan 19 14:55:00 2018 +0100 +++ b/src/Pure/PIDE/protocol.scala Fri Jan 19 14:55:46 2018 +0100 @@ -343,6 +343,7 @@ val base = resources.session_base.standard_path protocol_command("Prover.init_session_base", encode_list(base.known.sessions.toList), + encode_list(base.doc_names), encode_table(base.global_theories.toList), encode_list(base.loaded_theories.keys), encode_table(base.dest_known_theories)) diff -r d36fcde7e2c0 -r bddfa23a4ea9 src/Pure/PIDE/resources.ML --- a/src/Pure/PIDE/resources.ML Fri Jan 19 14:55:00 2018 +0100 +++ b/src/Pure/PIDE/resources.ML Fri Jan 19 14:55:46 2018 +0100 @@ -9,6 +9,7 @@ val default_qualifier: string val init_session_base: {sessions: string list, + doc_names: string list, global_theories: (string * string) list, loaded_theories: string list, known_theories: (string * string) list} -> unit @@ -17,6 +18,7 @@ val loaded_theory: string -> bool val known_theory: string -> Path.T option 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 @@ -45,6 +47,7 @@ val empty_session_base = {sessions = []: string list, + doc_names = []: string list, global_theories = Symtab.empty: string Symtab.table, loaded_theories = Symtab.empty: unit Symtab.table, known_theories = Symtab.empty: Path.T Symtab.table}; @@ -52,10 +55,11 @@ val global_session_base = Synchronized.var "Sessions.base" empty_session_base; -fun init_session_base {sessions, global_theories, loaded_theories, known_theories} = +fun init_session_base {sessions, doc_names, global_theories, loaded_theories, known_theories} = Synchronized.change global_session_base (fn _ => {sessions = sort_strings sessions, + doc_names = doc_names, global_theories = Symtab.make global_theories, loaded_theories = Symtab.make_set loaded_theories, known_theories = Symtab.make (map (apsnd Path.explode) known_theories)}); @@ -64,6 +68,7 @@ Synchronized.change global_session_base (fn {global_theories, loaded_theories, ...} => {sessions = [], + doc_names = [], global_theories = global_theories, loaded_theories = loaded_theories, known_theories = #known_theories empty_session_base}); @@ -74,21 +79,25 @@ fun loaded_theory a = Symtab.defined (get_session_base #loaded_theories) a; fun known_theory a = Symtab.lookup (get_session_base #known_theories) a; -fun check_session ctxt (name, pos) = - let val sessions = get_session_base #sessions in - if member (op =) sessions name then - (Context_Position.report ctxt pos (Markup.entity Markup.sessionN name); name) +fun check_name which kind markup ctxt (name, pos) = + let val names = get_session_base which in + if member (op =) names name then + (Context_Position.report ctxt pos (markup name); name) else let val completion = Completion.make (name, pos) (fn completed => - sessions + names |> filter completed - |> map (fn a => (a, (Markup.sessionN, a)))); + |> map (fn a => (a, (kind, a)))); val report = Markup.markup_report (Completion.reported_text completion); - in error ("Bad session " ^ quote name ^ Position.here pos ^ report) end + in error ("Bad " ^ kind ^ " " ^ quote name ^ Position.here pos ^ report) end end; +val check_session = check_name #sessions "session" (Markup.entity Markup.sessionN); +val check_doc = check_name #doc_names "documentation" Markup.doc; + + (* manage source files *) @@ -258,6 +267,8 @@ val _ = Theory.setup (Thy_Output.antiquotation_verbatim \<^binding>\session\ (Scan.lift (Parse.position Parse.embedded)) check_session #> + Thy_Output.antiquotation_verbatim \<^binding>\doc\ + (Scan.lift (Parse.position Parse.embedded)) check_doc #> Thy_Output.antiquotation_raw \<^binding>\path\ (Scan.lift (Parse.position Parse.path)) (document_antiq check_path) #> Thy_Output.antiquotation_raw \<^binding>\file\ diff -r d36fcde7e2c0 -r bddfa23a4ea9 src/Pure/Thy/document_antiquotations.ML --- a/src/Pure/Thy/document_antiquotations.ML Fri Jan 19 14:55:00 2018 +0100 +++ b/src/Pure/Thy/document_antiquotations.ML Fri Jan 19 14:55:46 2018 +0100 @@ -290,15 +290,6 @@ in Latex.enclose_block "\\url{" "}" [Latex.string url] end)); -(* doc entries *) - -val _ = Theory.setup - (Thy_Output.antiquotation_pretty \<^binding>\doc\ (Scan.lift (Parse.position Parse.embedded)) - (fn ctxt => fn (name, pos) => - let val _ = Context_Position.report ctxt pos (Markup.doc name) - in [Pretty.str name] end)); - - (* formal entities *) local diff -r d36fcde7e2c0 -r bddfa23a4ea9 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Fri Jan 19 14:55:00 2018 +0100 +++ b/src/Pure/Thy/sessions.scala Fri Jan 19 14:55:46 2018 +0100 @@ -129,6 +129,7 @@ sealed case class Base( pos: Position.T = Position.none, + doc_names: List[String] = Nil, global_theories: Map[String, String] = Map.empty, loaded_theories: Graph[String, Outer_Syntax] = Graph.string, known: Known = Known.empty, @@ -221,6 +222,8 @@ } } + val doc_names = Doc.doc_names() + val session_bases = (Map.empty[String, Base] /: sessions_structure.imports_topological_order)({ case (session_bases, session_name) => @@ -328,6 +331,7 @@ val base = Base( pos = info.pos, + doc_names = doc_names, global_theories = global_theories, loaded_theories = dependencies.loaded_theories, known = known, diff -r d36fcde7e2c0 -r bddfa23a4ea9 src/Pure/Tools/build.ML --- a/src/Pure/Tools/build.ML Fri Jan 19 14:55:00 2018 +0100 +++ b/src/Pure/Tools/build.ML Fri Jan 19 14:55:46 2018 +0100 @@ -150,6 +150,7 @@ master_dir: Path.T, theories: (Options.T * (string * Position.T) list) list, sessions: string list, + doc_names: string list, global_theories: (string * string) list, loaded_theories: string list, known_theories: (string * string) list, @@ -161,14 +162,14 @@ val position = Position.of_properties o properties; val (symbol_codes, (command_timings, (do_output, (verbose, (browser_info, (document_files, (graph_file, (parent_name, (chapter, (name, (master_dir, - (theories, (sessions, (global_theories, (loaded_theories, - (known_theories, bibtex_entries)))))))))))))))) = + (theories, (sessions, (doc_names, (global_theories, (loaded_theories, + (known_theories, bibtex_entries))))))))))))))))) = pair (list (pair string int)) (pair (list properties) (pair bool (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 string) (pair (list (pair string string)) (pair (list string) - (pair (list (pair string string)) (list string)))))))))))))))) + (pair (list string) (pair (list string) (pair (list (pair string string)) (pair (list string) + (pair (list (pair string string)) (list string))))))))))))))))) (YXML.parse_body yxml); in Args {symbol_codes = symbol_codes, command_timings = command_timings, do_output = do_output, @@ -176,19 +177,20 @@ 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, sessions = sessions, - global_theories = global_theories, loaded_theories = loaded_theories, + doc_names = doc_names, global_theories = global_theories, loaded_theories = loaded_theories, known_theories = known_theories, bibtex_entries = bibtex_entries} end; fun build_session (Args {symbol_codes, command_timings, do_output, verbose, browser_info, document_files, graph_file, parent_name, chapter, name, master_dir, theories, sessions, - global_theories, loaded_theories, known_theories, bibtex_entries}) = + doc_names, global_theories, loaded_theories, known_theories, bibtex_entries}) = let val symbols = HTML.make_symbols symbol_codes; val _ = Resources.init_session_base {sessions = sessions, + doc_names = doc_names, global_theories = global_theories, loaded_theories = loaded_theories, known_theories = known_theories}; diff -r d36fcde7e2c0 -r bddfa23a4ea9 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Fri Jan 19 14:55:00 2018 +0100 +++ b/src/Pure/Tools/build.scala Fri Jan 19 14:55:46 2018 +0100 @@ -212,16 +212,14 @@ pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string, pair(string, pair(string, pair(string, pair(Path.encode, pair(list(pair(Options.encode, list(pair(string, properties)))), - pair(list(string), pair(list(pair(string, string)), pair(list(string), - pair(list(pair(string, string)), list(string)))))))))))))))))( + pair(list(string), pair(list(string), pair(list(pair(string, string)), + pair(list(string), pair(list(pair(string, string)), list(string))))))))))))))))))( (Symbol.codes, (command_timings, (do_output, (verbose, (store.browser_info, (info.document_files, (File.standard_path(graph_file), (parent, (info.chapter, (name, (Path.current, - (info.theories, (base.known.sessions.toList, - (base.global_theories.toList, - (base.loaded_theories.keys, - (base.dest_known_theories, - info.bibtex_entries.map(_.info)))))))))))))))))) + (info.theories, (base.known.sessions.toList, (base.doc_names, + (base.global_theories.toList, (base.loaded_theories.keys, (base.dest_known_theories, + info.bibtex_entries.map(_.info))))))))))))))))))) }) val env = diff -r d36fcde7e2c0 -r bddfa23a4ea9 src/Pure/Tools/doc.scala --- a/src/Pure/Tools/doc.scala Fri Jan 19 14:55:00 2018 +0100 +++ b/src/Pure/Tools/doc.scala Fri Jan 19 14:55:46 2018 +0100 @@ -77,6 +77,9 @@ examples() ::: release_notes() ::: main_contents } + def doc_names(): List[String] = + for (Doc(name, _, _) <- contents()) yield name + /* view */