--- 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) + "}")
--- 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}
--- 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))
--- 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>\<open>session\<close>
(Scan.lift (Parse.position Parse.embedded)) check_session #>
+ Thy_Output.antiquotation_verbatim \<^binding>\<open>doc\<close>
+ (Scan.lift (Parse.position Parse.embedded)) check_doc #>
Thy_Output.antiquotation_raw \<^binding>\<open>path\<close>
(Scan.lift (Parse.position Parse.path)) (document_antiq check_path) #>
Thy_Output.antiquotation_raw \<^binding>\<open>file\<close>
--- 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>\<open>doc\<close> (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
--- 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,
--- 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};
--- 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 =
--- 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 */