formal treatment of documentation names;
authorwenzelm
Fri Jan 19 14:55:46 2018 +0100 (20 months ago ago)
changeset 67472bddfa23a4ea9
parent 67471 d36fcde7e2c0
child 67473 7ed8d4cdfb13
formal treatment of documentation names;
src/Pure/ML/ml_process.scala
src/Pure/PIDE/protocol.ML
src/Pure/PIDE/protocol.scala
src/Pure/PIDE/resources.ML
src/Pure/Thy/document_antiquotations.ML
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.ML
src/Pure/Tools/build.scala
src/Pure/Tools/doc.scala
     1.1 --- a/src/Pure/ML/ml_process.scala	Fri Jan 19 14:55:00 2018 +0100
     1.2 +++ b/src/Pure/ML/ml_process.scala	Fri Jan 19 14:55:46 2018 +0100
     1.3 @@ -103,6 +103,7 @@
     1.4              ML_Syntax.print_list(ML_Syntax.print_string_bytes)(list)
     1.5            List("Resources.init_session_base" +
     1.6              " {sessions = " + print_list(base.known.sessions.toList) +
     1.7 +            ", doc_names = " + print_list(base.doc_names) +
     1.8              ", global_theories = " + print_table(base.global_theories.toList) +
     1.9              ", loaded_theories = " + print_list(base.loaded_theories.keys) +
    1.10              ", known_theories = " + print_table(base.dest_known_theories) + "}")
     2.1 --- a/src/Pure/PIDE/protocol.ML	Fri Jan 19 14:55:00 2018 +0100
     2.2 +++ b/src/Pure/PIDE/protocol.ML	Fri Jan 19 14:55:46 2018 +0100
     2.3 @@ -19,13 +19,15 @@
     2.4  
     2.5  val _ =
     2.6    Isabelle_Process.protocol_command "Prover.init_session_base"
     2.7 -    (fn [sessions_yxml, global_theories_yxml, loaded_theories_yxml, known_theories_yxml] =>
     2.8 +    (fn [sessions_yxml, doc_names_yxml, global_theories_yxml, loaded_theories_yxml,
     2.9 +          known_theories_yxml] =>
    2.10        let
    2.11          val decode_table = YXML.parse_body #> let open XML.Decode in list (pair string string) end;
    2.12          val decode_list = YXML.parse_body #> let open XML.Decode in list string end;
    2.13        in
    2.14          Resources.init_session_base
    2.15            {sessions = decode_list sessions_yxml,
    2.16 +           doc_names = decode_list doc_names_yxml,
    2.17             global_theories = decode_table global_theories_yxml,
    2.18             loaded_theories = decode_list loaded_theories_yxml,
    2.19             known_theories = decode_table known_theories_yxml}
     3.1 --- a/src/Pure/PIDE/protocol.scala	Fri Jan 19 14:55:00 2018 +0100
     3.2 +++ b/src/Pure/PIDE/protocol.scala	Fri Jan 19 14:55:46 2018 +0100
     3.3 @@ -343,6 +343,7 @@
     3.4      val base = resources.session_base.standard_path
     3.5      protocol_command("Prover.init_session_base",
     3.6        encode_list(base.known.sessions.toList),
     3.7 +      encode_list(base.doc_names),
     3.8        encode_table(base.global_theories.toList),
     3.9        encode_list(base.loaded_theories.keys),
    3.10        encode_table(base.dest_known_theories))
     4.1 --- a/src/Pure/PIDE/resources.ML	Fri Jan 19 14:55:00 2018 +0100
     4.2 +++ b/src/Pure/PIDE/resources.ML	Fri Jan 19 14:55:46 2018 +0100
     4.3 @@ -9,6 +9,7 @@
     4.4    val default_qualifier: string
     4.5    val init_session_base:
     4.6      {sessions: string list,
     4.7 +     doc_names: string list,
     4.8       global_theories: (string * string) list,
     4.9       loaded_theories: string list,
    4.10       known_theories: (string * string) list} -> unit
    4.11 @@ -17,6 +18,7 @@
    4.12    val loaded_theory: string -> bool
    4.13    val known_theory: string -> Path.T option
    4.14    val check_session: Proof.context -> string * Position.T -> string
    4.15 +  val check_doc: Proof.context -> string * Position.T -> string
    4.16    val master_directory: theory -> Path.T
    4.17    val imports_of: theory -> (string * Position.T) list
    4.18    val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
    4.19 @@ -45,6 +47,7 @@
    4.20  
    4.21  val empty_session_base =
    4.22    {sessions = []: string list,
    4.23 +   doc_names = []: string list,
    4.24     global_theories = Symtab.empty: string Symtab.table,
    4.25     loaded_theories = Symtab.empty: unit Symtab.table,
    4.26     known_theories = Symtab.empty: Path.T Symtab.table};
    4.27 @@ -52,10 +55,11 @@
    4.28  val global_session_base =
    4.29    Synchronized.var "Sessions.base" empty_session_base;
    4.30  
    4.31 -fun init_session_base {sessions, global_theories, loaded_theories, known_theories} =
    4.32 +fun init_session_base {sessions, doc_names, global_theories, loaded_theories, known_theories} =
    4.33    Synchronized.change global_session_base
    4.34      (fn _ =>
    4.35        {sessions = sort_strings sessions,
    4.36 +       doc_names = doc_names,
    4.37         global_theories = Symtab.make global_theories,
    4.38         loaded_theories = Symtab.make_set loaded_theories,
    4.39         known_theories = Symtab.make (map (apsnd Path.explode) known_theories)});
    4.40 @@ -64,6 +68,7 @@
    4.41    Synchronized.change global_session_base
    4.42      (fn {global_theories, loaded_theories, ...} =>
    4.43        {sessions = [],
    4.44 +       doc_names = [],
    4.45         global_theories = global_theories,
    4.46         loaded_theories = loaded_theories,
    4.47         known_theories = #known_theories empty_session_base});
    4.48 @@ -74,21 +79,25 @@
    4.49  fun loaded_theory a = Symtab.defined (get_session_base #loaded_theories) a;
    4.50  fun known_theory a = Symtab.lookup (get_session_base #known_theories) a;
    4.51  
    4.52 -fun check_session ctxt (name, pos) =
    4.53 -  let val sessions = get_session_base #sessions in
    4.54 -    if member (op =) sessions name then
    4.55 -      (Context_Position.report ctxt pos (Markup.entity Markup.sessionN name); name)
    4.56 +fun check_name which kind markup ctxt (name, pos) =
    4.57 +  let val names = get_session_base which in
    4.58 +    if member (op =) names name then
    4.59 +      (Context_Position.report ctxt pos (markup name); name)
    4.60      else
    4.61        let
    4.62          val completion =
    4.63            Completion.make (name, pos) (fn completed =>
    4.64 -              sessions
    4.65 +              names
    4.66                |> filter completed
    4.67 -              |> map (fn a => (a, (Markup.sessionN, a))));
    4.68 +              |> map (fn a => (a, (kind, a))));
    4.69          val report = Markup.markup_report (Completion.reported_text completion);
    4.70 -      in error ("Bad session " ^ quote name ^ Position.here pos ^ report) end
    4.71 +      in error ("Bad " ^ kind ^ " " ^ quote name ^ Position.here pos ^ report) end
    4.72    end;
    4.73  
    4.74 +val check_session = check_name #sessions "session" (Markup.entity Markup.sessionN);
    4.75 +val check_doc = check_name #doc_names "documentation" Markup.doc;
    4.76 +
    4.77 +
    4.78  
    4.79  (* manage source files *)
    4.80  
    4.81 @@ -258,6 +267,8 @@
    4.82  val _ = Theory.setup
    4.83   (Thy_Output.antiquotation_verbatim \<^binding>\<open>session\<close>
    4.84      (Scan.lift (Parse.position Parse.embedded)) check_session #>
    4.85 +  Thy_Output.antiquotation_verbatim \<^binding>\<open>doc\<close>
    4.86 +    (Scan.lift (Parse.position Parse.embedded)) check_doc #>
    4.87    Thy_Output.antiquotation_raw \<^binding>\<open>path\<close>
    4.88      (Scan.lift (Parse.position Parse.path)) (document_antiq check_path) #>
    4.89    Thy_Output.antiquotation_raw \<^binding>\<open>file\<close>
     5.1 --- a/src/Pure/Thy/document_antiquotations.ML	Fri Jan 19 14:55:00 2018 +0100
     5.2 +++ b/src/Pure/Thy/document_antiquotations.ML	Fri Jan 19 14:55:46 2018 +0100
     5.3 @@ -290,15 +290,6 @@
     5.4        in Latex.enclose_block "\\url{" "}" [Latex.string url] end));
     5.5  
     5.6  
     5.7 -(* doc entries *)
     5.8 -
     5.9 -val _ = Theory.setup
    5.10 -  (Thy_Output.antiquotation_pretty \<^binding>\<open>doc\<close> (Scan.lift (Parse.position Parse.embedded))
    5.11 -    (fn ctxt => fn (name, pos) =>
    5.12 -      let val _ = Context_Position.report ctxt pos (Markup.doc name)
    5.13 -      in [Pretty.str name] end));
    5.14 -
    5.15 -
    5.16  (* formal entities *)
    5.17  
    5.18  local
     6.1 --- a/src/Pure/Thy/sessions.scala	Fri Jan 19 14:55:00 2018 +0100
     6.2 +++ b/src/Pure/Thy/sessions.scala	Fri Jan 19 14:55:46 2018 +0100
     6.3 @@ -129,6 +129,7 @@
     6.4  
     6.5    sealed case class Base(
     6.6      pos: Position.T = Position.none,
     6.7 +    doc_names: List[String] = Nil,
     6.8      global_theories: Map[String, String] = Map.empty,
     6.9      loaded_theories: Graph[String, Outer_Syntax] = Graph.string,
    6.10      known: Known = Known.empty,
    6.11 @@ -221,6 +222,8 @@
    6.12        }
    6.13      }
    6.14  
    6.15 +    val doc_names = Doc.doc_names()
    6.16 +
    6.17      val session_bases =
    6.18        (Map.empty[String, Base] /: sessions_structure.imports_topological_order)({
    6.19          case (session_bases, session_name) =>
    6.20 @@ -328,6 +331,7 @@
    6.21              val base =
    6.22                Base(
    6.23                  pos = info.pos,
    6.24 +                doc_names = doc_names,
    6.25                  global_theories = global_theories,
    6.26                  loaded_theories = dependencies.loaded_theories,
    6.27                  known = known,
     7.1 --- a/src/Pure/Tools/build.ML	Fri Jan 19 14:55:00 2018 +0100
     7.2 +++ b/src/Pure/Tools/build.ML	Fri Jan 19 14:55:46 2018 +0100
     7.3 @@ -150,6 +150,7 @@
     7.4    master_dir: Path.T,
     7.5    theories: (Options.T * (string * Position.T) list) list,
     7.6    sessions: string list,
     7.7 +  doc_names: string list,
     7.8    global_theories: (string * string) list,
     7.9    loaded_theories: string list,
    7.10    known_theories: (string * string) list,
    7.11 @@ -161,14 +162,14 @@
    7.12      val position = Position.of_properties o properties;
    7.13      val (symbol_codes, (command_timings, (do_output, (verbose, (browser_info,
    7.14        (document_files, (graph_file, (parent_name, (chapter, (name, (master_dir,
    7.15 -      (theories, (sessions, (global_theories, (loaded_theories,
    7.16 -      (known_theories, bibtex_entries)))))))))))))))) =
    7.17 +      (theories, (sessions, (doc_names, (global_theories, (loaded_theories,
    7.18 +      (known_theories, bibtex_entries))))))))))))))))) =
    7.19        pair (list (pair string int)) (pair (list properties) (pair bool (pair bool (pair string
    7.20          (pair (list (pair string string)) (pair string (pair string (pair string (pair string
    7.21            (pair string
    7.22              (pair (((list (pair Options.decode (list (pair string position))))))
    7.23 -              (pair (list string) (pair (list (pair string string)) (pair (list string)
    7.24 -                (pair (list (pair string string)) (list string))))))))))))))))
    7.25 +              (pair (list string) (pair (list string) (pair (list (pair string string)) (pair (list string)
    7.26 +                (pair (list (pair string string)) (list string)))))))))))))))))
    7.27        (YXML.parse_body yxml);
    7.28    in
    7.29      Args {symbol_codes = symbol_codes, command_timings = command_timings, do_output = do_output,
    7.30 @@ -176,19 +177,20 @@
    7.31        document_files = map (apply2 Path.explode) document_files,
    7.32        graph_file = Path.explode graph_file, parent_name = parent_name, chapter = chapter,
    7.33        name = name, master_dir = Path.explode master_dir, theories = theories, sessions = sessions,
    7.34 -      global_theories = global_theories, loaded_theories = loaded_theories,
    7.35 +      doc_names = doc_names, global_theories = global_theories, loaded_theories = loaded_theories,
    7.36        known_theories = known_theories, bibtex_entries = bibtex_entries}
    7.37    end;
    7.38  
    7.39  fun build_session (Args {symbol_codes, command_timings, do_output, verbose, browser_info,
    7.40      document_files, graph_file, parent_name, chapter, name, master_dir, theories, sessions,
    7.41 -    global_theories, loaded_theories, known_theories, bibtex_entries}) =
    7.42 +    doc_names, global_theories, loaded_theories, known_theories, bibtex_entries}) =
    7.43    let
    7.44      val symbols = HTML.make_symbols symbol_codes;
    7.45  
    7.46      val _ =
    7.47        Resources.init_session_base
    7.48          {sessions = sessions,
    7.49 +         doc_names = doc_names,
    7.50           global_theories = global_theories,
    7.51           loaded_theories = loaded_theories,
    7.52           known_theories = known_theories};
     8.1 --- a/src/Pure/Tools/build.scala	Fri Jan 19 14:55:00 2018 +0100
     8.2 +++ b/src/Pure/Tools/build.scala	Fri Jan 19 14:55:46 2018 +0100
     8.3 @@ -212,16 +212,14 @@
     8.4                  pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
     8.5                  pair(string, pair(string, pair(string, pair(Path.encode,
     8.6                  pair(list(pair(Options.encode, list(pair(string, properties)))),
     8.7 -                pair(list(string), pair(list(pair(string, string)), pair(list(string),
     8.8 -                pair(list(pair(string, string)), list(string)))))))))))))))))(
     8.9 +                pair(list(string), pair(list(string), pair(list(pair(string, string)),
    8.10 +                pair(list(string), pair(list(pair(string, string)), list(string))))))))))))))))))(
    8.11                (Symbol.codes, (command_timings, (do_output, (verbose,
    8.12                  (store.browser_info, (info.document_files, (File.standard_path(graph_file),
    8.13                  (parent, (info.chapter, (name, (Path.current,
    8.14 -                (info.theories, (base.known.sessions.toList,
    8.15 -                (base.global_theories.toList,
    8.16 -                (base.loaded_theories.keys,
    8.17 -                (base.dest_known_theories,
    8.18 -                info.bibtex_entries.map(_.info))))))))))))))))))
    8.19 +                (info.theories, (base.known.sessions.toList, (base.doc_names,
    8.20 +                (base.global_theories.toList, (base.loaded_theories.keys, (base.dest_known_theories,
    8.21 +                info.bibtex_entries.map(_.info)))))))))))))))))))
    8.22              })
    8.23  
    8.24          val env =
     9.1 --- a/src/Pure/Tools/doc.scala	Fri Jan 19 14:55:00 2018 +0100
     9.2 +++ b/src/Pure/Tools/doc.scala	Fri Jan 19 14:55:46 2018 +0100
     9.3 @@ -77,6 +77,9 @@
     9.4      examples() ::: release_notes() ::: main_contents
     9.5    }
     9.6  
     9.7 +  def doc_names(): List[String] =
     9.8 +    for (Doc(name, _, _) <- contents()) yield name
     9.9 +
    9.10  
    9.11    /* view */
    9.12