--- a/src/Pure/PIDE/resources.ML Sat Nov 28 16:25:29 2020 +0100
+++ b/src/Pure/PIDE/resources.ML Sat Nov 28 17:38:03 2020 +0100
@@ -13,7 +13,6 @@
session_chapters: (string * string) list,
bibtex_entries: (string * string list) list,
command_timings: Properties.T list,
- docs: string list,
scala_functions: (string * Position.T) list,
global_theories: (string * string) list,
loaded_theories: string list} -> unit
@@ -25,7 +24,6 @@
val check_session: Proof.context -> string * Position.T -> string
val session_chapter: string -> string
val last_timing: Toplevel.transition -> Time.time
- val check_doc: Proof.context -> string * Position.T -> string
val scala_function_pos: string -> Position.T
val master_directory: theory -> Path.T
val imports_of: theory -> (string * Position.T) list
@@ -104,7 +102,6 @@
session_chapters = Symtab.empty: string Symtab.table,
bibtex_entries = Symtab.empty: string list Symtab.table,
timings = empty_timings,
- docs = []: (string * entry) list,
scala_functions = Symtab.empty: Position.T Symtab.table},
{global_theories = Symtab.empty: string Symtab.table,
loaded_theories = Symtab.empty: unit Symtab.table});
@@ -114,7 +111,7 @@
fun init_session
{session_positions, session_directories, session_chapters, bibtex_entries,
- command_timings, docs, scala_functions, global_theories, loaded_theories} =
+ command_timings, scala_functions, global_theories, loaded_theories} =
Synchronized.change global_session_base
(fn _ =>
({session_positions = sort_by #1 (map (apsnd make_entry) session_positions),
@@ -124,7 +121,6 @@
session_chapters = Symtab.make session_chapters,
bibtex_entries = Symtab.make bibtex_entries,
timings = make_timings command_timings,
- docs = sort_by #1 (map (apsnd make_entry o rpair []) docs),
scala_functions = Symtab.make scala_functions},
{global_theories = Symtab.make global_theories,
loaded_theories = Symtab.make_set loaded_theories}));
@@ -132,15 +128,14 @@
fun init_session_yxml yxml =
let
val (session_positions, (session_directories, (session_chapters, (bibtex_entries,
- (command_timings, (docs, (scala_functions, (global_theories, loaded_theories)))))))) =
+ (command_timings, (scala_functions, (global_theories, loaded_theories))))))) =
YXML.parse_body yxml |>
let open XML.Decode in
(pair (list (pair string properties))
(pair (list (pair string string)) (pair (list (pair string string))
(pair (list (pair string (list string))) (pair (list properties)
- (pair (list string)
- (pair (list (pair string properties))
- (pair (list (pair string string)) (list string)))))))))
+ (pair (list (pair string properties))
+ (pair (list (pair string string)) (list string))))))))
end;
in
init_session
@@ -149,7 +144,6 @@
session_chapters = session_chapters,
bibtex_entries = bibtex_entries,
command_timings = command_timings,
- docs = docs,
scala_functions = map (apsnd Position.of_properties) scala_functions,
global_theories = global_theories,
loaded_theories = loaded_theories}
@@ -169,22 +163,18 @@
fun global_theory a = Symtab.lookup (get_session_base2 #global_theories) a;
fun loaded_theory a = Symtab.defined (get_session_base2 #loaded_theories) a;
-fun check_name which kind markup ctxt arg =
- Completion.check_item kind markup (get_session_base1 which |> sort_by #1) ctxt arg;
-
-val check_session =
- check_name #session_positions "session"
+fun check_session ctxt arg =
+ Completion.check_item "session"
(fn (name, {pos, serial}) =>
Markup.entity Markup.sessionN name
- |> Markup.properties (Position.entity_properties_of false serial pos));
+ |> Markup.properties (Position.entity_properties_of false serial pos))
+ (get_session_base1 #session_positions) ctxt arg;
fun session_chapter name =
the_default "Unsorted" (Symtab.lookup (get_session_base1 #session_chapters) name);
fun last_timing tr = get_timings (get_session_base1 #timings) tr;
-val check_doc = check_name #docs "documentation" (Markup.doc o #1);
-
fun scala_function_pos name =
Symtab.lookup (get_session_base1 #scala_functions) name
|> the_default Position.none;
@@ -386,8 +376,6 @@
val _ = Theory.setup
(Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>session\<close>
(Scan.lift Parse.embedded_position) check_session #>
- Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>doc\<close>
- (Scan.lift Parse.embedded_position) check_doc #>
Thy_Output.antiquotation_raw_embedded \<^binding>\<open>path\<close> (document_antiq check_path) (K I) #>
Thy_Output.antiquotation_raw_embedded \<^binding>\<open>file\<close> (document_antiq check_file) (K I) #>
Thy_Output.antiquotation_raw_embedded \<^binding>\<open>dir\<close> (document_antiq check_dir) (K I) #>
--- a/src/Pure/PIDE/resources.scala Sat Nov 28 16:25:29 2020 +0100
+++ b/src/Pure/PIDE/resources.scala Sat Nov 28 17:38:03 2020 +0100
@@ -33,18 +33,16 @@
pair(list(pair(string, string)),
pair(list(pair(string, list(string))),
pair(list(properties),
- pair(list(string),
pair(list(pair(string, properties)),
- pair(list(pair(string, string)), list(string)))))))))(
+ pair(list(pair(string, string)), list(string))))))))(
(sessions_structure.session_positions,
(sessions_structure.dest_session_directories,
(sessions_structure.session_chapters,
(sessions_structure.bibtex_entries,
(command_timings,
- (session_base.doc_names,
(Scala.functions.map(fun => (fun.name, fun.position)),
(session_base.global_theories.toList,
- session_base.loaded_theories.keys))))))))))
+ session_base.loaded_theories.keys)))))))))
}
--- a/src/Pure/ROOT.ML Sat Nov 28 16:25:29 2020 +0100
+++ b/src/Pure/ROOT.ML Sat Nov 28 17:38:03 2020 +0100
@@ -349,6 +349,7 @@
ML_file "Tools/simplifier_trace.ML";
ML_file_no_debug "Tools/debugger.ML";
ML_file "Tools/named_theorems.ML";
+ML_file "Tools/doc.ML";
ML_file "Tools/jedit.ML";
ML_file "Tools/ghc.ML";
ML_file "Tools/generated_files.ML"
--- a/src/Pure/System/scala.scala Sat Nov 28 16:25:29 2020 +0100
+++ b/src/Pure/System/scala.scala Sat Nov 28 17:38:03 2020 +0100
@@ -242,4 +242,5 @@
Scala.Echo,
Scala.Sleep,
Scala.Toplevel,
+ Doc.Doc_Names,
Bibtex.Check_Database)
--- a/src/Pure/Thy/sessions.scala Sat Nov 28 16:25:29 2020 +0100
+++ b/src/Pure/Thy/sessions.scala Sat Nov 28 17:38:03 2020 +0100
@@ -49,7 +49,6 @@
sealed case class Base(
pos: Position.T = Position.none,
- doc_names: List[String] = Nil,
session_directories: Map[JFile, String] = Map.empty,
global_theories: Map[String, String] = Map.empty,
session_theories: List[Document.Node.Name] = Nil,
@@ -142,8 +141,6 @@
}
}
- val doc_names = Doc.doc_names()
-
val bootstrap =
Sessions.Base.bootstrap(
sessions_structure.session_directories,
@@ -325,7 +322,6 @@
val base =
Base(
pos = info.pos,
- doc_names = doc_names,
session_directories = sessions_structure.session_directories,
global_theories = sessions_structure.global_theories,
session_theories = session_theories,
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/doc.ML Sat Nov 28 17:38:03 2020 +0100
@@ -0,0 +1,24 @@
+(* Title: Pure/Tools/doc.ML
+ Author: Makarius
+
+Access to Isabelle documentation.
+*)
+
+signature DOC =
+sig
+ val check: Proof.context -> string * Position.T -> string
+end;
+
+structure Doc: DOC =
+struct
+
+fun check ctxt arg =
+ Completion.check_item "documentation" (Markup.doc o #1)
+ (\<^scala>\<open>doc_names\<close> "" |> split_lines |> map (rpair ())) ctxt arg;
+
+val _ =
+ Theory.setup
+ (Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>doc\<close>
+ (Scan.lift Parse.embedded_position) check);
+
+end;
--- a/src/Pure/Tools/doc.scala Sat Nov 28 16:25:29 2020 +0100
+++ b/src/Pure/Tools/doc.scala Sat Nov 28 17:38:03 2020 +0100
@@ -76,8 +76,13 @@
examples() ::: release_notes() ::: main_contents
}
- def doc_names(): List[String] =
- for (Doc(name, _, _) <- contents()) yield name
+ object Doc_Names extends Scala.Fun("doc_names")
+ {
+ val here = Scala_Project.here
+ def apply(arg: String): String =
+ if (arg.nonEmpty) error("Bad argument: " + quote(arg))
+ else cat_lines((for (Doc(name, _, _) <- contents()) yield name).sorted)
+ }
/* view */