# HG changeset patch
# User wenzelm
# Date 1606581483 -3600
# Node ID 0421805400683880be1051b7021161aa90a05f14
# Parent  bd5ee31481322f1dd73be696aa5dd992eb611f7f
clarified protocol: Doc.check at run-time via Scala function;

diff -r bd5ee3148132 -r 042180540068 src/Pure/PIDE/resources.ML
--- 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) #>
diff -r bd5ee3148132 -r 042180540068 src/Pure/PIDE/resources.scala
--- 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)))))))))
   }
 
 
diff -r bd5ee3148132 -r 042180540068 src/Pure/ROOT.ML
--- 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"
diff -r bd5ee3148132 -r 042180540068 src/Pure/System/scala.scala
--- 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)
diff -r bd5ee3148132 -r 042180540068 src/Pure/Thy/sessions.scala
--- 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,
diff -r bd5ee3148132 -r 042180540068 src/Pure/Tools/doc.ML
--- /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;
diff -r bd5ee3148132 -r 042180540068 src/Pure/Tools/doc.scala
--- 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 */