added document antiquotation @{session name};
authorwenzelm
Sat Dec 16 21:53:07 2017 +0100 (17 months ago)
changeset 6721981e9804b2014
parent 67218 e62d72699666
child 67220 0049bed35f5a
added document antiquotation @{session name};
renamed protocol function "Prover.session_base" to "Prover.init_session_base" according to the ML/Scala operation;
NEWS
src/Doc/Isar_Ref/Document_Preparation.thy
src/Doc/ROOT
src/Doc/System/Presentation.thy
src/Pure/ML/ml_process.scala
src/Pure/PIDE/markup.ML
src/Pure/PIDE/protocol.ML
src/Pure/PIDE/protocol.scala
src/Pure/PIDE/resources.ML
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.ML
src/Pure/Tools/build.scala
     1.1 --- a/NEWS	Sat Dec 16 20:02:40 2017 +0100
     1.2 +++ b/NEWS	Sat Dec 16 21:53:07 2017 +0100
     1.3 @@ -85,6 +85,9 @@
     1.4  antiquotations in control symbol notation, e.g. \<^const_name> becomes
     1.5  \isactrlconstUNDERSCOREname.
     1.6  
     1.7 +* Document antiquotation @{session name} checks and prints the given
     1.8 +session name verbatim.
     1.9 +
    1.10  * Document preparation with skip_proofs option now preserves the content
    1.11  more accurately: only terminal proof steps ('by' etc.) are skipped.
    1.12  
     2.1 --- a/src/Doc/Isar_Ref/Document_Preparation.thy	Sat Dec 16 20:02:40 2017 +0100
     2.2 +++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Sat Dec 16 21:53:07 2017 +0100
     2.3 @@ -107,6 +107,7 @@
     2.4      @{antiquotation_def emph} & : & \<open>antiquotation\<close> \\
     2.5      @{antiquotation_def bold} & : & \<open>antiquotation\<close> \\
     2.6      @{antiquotation_def verbatim} & : & \<open>antiquotation\<close> \\
     2.7 +    @{antiquotation_def session} & : & \<open>antiquotation\<close> \\
     2.8      @{antiquotation_def "file"} & : & \<open>antiquotation\<close> \\
     2.9      @{antiquotation_def "url"} & : & \<open>antiquotation\<close> \\
    2.10      @{antiquotation_def "cite"} & : & \<open>antiquotation\<close> \\
    2.11 @@ -195,6 +196,7 @@
    2.12        @@{antiquotation emph} options @{syntax text} |
    2.13        @@{antiquotation bold} options @{syntax text} |
    2.14        @@{antiquotation verbatim} options @{syntax text} |
    2.15 +      @@{antiquotation session} options @{syntax embedded} |
    2.16        @@{antiquotation path} options @{syntax embedded} |
    2.17        @@{antiquotation "file"} options @{syntax name} |
    2.18        @@{antiquotation dir} options @{syntax name} |
    2.19 @@ -284,6 +286,9 @@
    2.20    \<^descr> \<open>@{verbatim s}\<close> prints uninterpreted source text literally as ASCII
    2.21    characters, using some type-writer font style.
    2.22  
    2.23 +  \<^descr> \<open>@{session name}\<close> prints given session name verbatim. The name is checked
    2.24 +  wrt.\ the dependencies of the current session.
    2.25 +
    2.26    \<^descr> \<open>@{path name}\<close> prints the file-system path name verbatim.
    2.27  
    2.28    \<^descr> \<open>@{file name}\<close> is like \<open>@{path name}\<close>, but ensures that \<open>name\<close> refers to a
     3.1 --- a/src/Doc/ROOT	Sat Dec 16 20:02:40 2017 +0100
     3.2 +++ b/src/Doc/ROOT	Sat Dec 16 21:53:07 2017 +0100
     3.3 @@ -372,6 +372,8 @@
     3.4  
     3.5  session System (doc) in "System" = Pure +
     3.6    options [document_variants = "system", thy_output_source]
     3.7 +  sessions
     3.8 +    "HOL-Library"
     3.9    theories
    3.10      Environment
    3.11      Sessions
     4.1 --- a/src/Doc/System/Presentation.thy	Sat Dec 16 20:02:40 2017 +0100
     4.2 +++ b/src/Doc/System/Presentation.thy	Sat Dec 16 21:53:07 2017 +0100
     4.3 @@ -69,9 +69,9 @@
     4.4    The presentation output will appear in \<^verbatim>\<open>$ISABELLE_BROWSER_INFO/FOL/FOL\<close> as
     4.5    reported by the above verbose invocation of the build process.
     4.6  
     4.7 -  Many Isabelle sessions (such as \<^verbatim>\<open>HOL-Library\<close> in \<^dir>\<open>~~/src/HOL/Library\<close>)
     4.8 -  also provide printable documents in PDF. These are prepared automatically as
     4.9 -  well if enabled like this:
    4.10 +  Many Isabelle sessions (such as \<^session>\<open>HOL-Library\<close> in
    4.11 +  \<^dir>\<open>~~/src/HOL/Library\<close>) also provide printable documents in PDF. These are
    4.12 +  prepared automatically as well if enabled like this:
    4.13    @{verbatim [display] \<open>isabelle build -o browser_info -o document=pdf -v -c HOL-Library\<close>}
    4.14  
    4.15    Enabling both browser info and document preparation simultaneously causes an
     5.1 --- a/src/Pure/ML/ml_process.scala	Sat Dec 16 20:02:40 2017 +0100
     5.2 +++ b/src/Pure/ML/ml_process.scala	Sat Dec 16 21:53:07 2017 +0100
     5.3 @@ -102,7 +102,8 @@
     5.4            def print_list(list: List[String]): String =
     5.5              ML_Syntax.print_list(ML_Syntax.print_string_bytes)(list)
     5.6            List("Resources.init_session_base" +
     5.7 -            " {global_theories = " + print_table(base.global_theories.toList) +
     5.8 +            " {sessions = " + print_list(base.known.sessions.toList) +
     5.9 +            ", global_theories = " + print_table(base.global_theories.toList) +
    5.10              ", loaded_theories = " + print_list(base.loaded_theories.keys) +
    5.11              ", known_theories = " + print_table(base.dest_known_theories) + "}")
    5.12        }
     6.1 --- a/src/Pure/PIDE/markup.ML	Sat Dec 16 20:02:40 2017 +0100
     6.2 +++ b/src/Pure/PIDE/markup.ML	Sat Dec 16 21:53:07 2017 +0100
     6.3 @@ -72,6 +72,7 @@
     6.4    val wordsN: string val words: T
     6.5    val hiddenN: string val hidden: T
     6.6    val system_optionN: string
     6.7 +  val sessionN: string
     6.8    val theoryN: string
     6.9    val classN: string
    6.10    val type_nameN: string
    6.11 @@ -394,6 +395,8 @@
    6.12  
    6.13  val system_optionN = "system_option";
    6.14  
    6.15 +val sessionN = "session";
    6.16 +
    6.17  val theoryN = "theory";
    6.18  val classN = "class";
    6.19  val type_nameN = "type_name";
     7.1 --- a/src/Pure/PIDE/protocol.ML	Sat Dec 16 20:02:40 2017 +0100
     7.2 +++ b/src/Pure/PIDE/protocol.ML	Sat Dec 16 21:53:07 2017 +0100
     7.3 @@ -18,14 +18,15 @@
     7.4         Isabelle_Process.init_options_interactive ()));
     7.5  
     7.6  val _ =
     7.7 -  Isabelle_Process.protocol_command "Prover.session_base"
     7.8 -    (fn [global_theories_yxml, loaded_theories_yxml, known_theories_yxml] =>
     7.9 +  Isabelle_Process.protocol_command "Prover.init_session_base"
    7.10 +    (fn [sessions_yxml, global_theories_yxml, loaded_theories_yxml, known_theories_yxml] =>
    7.11        let
    7.12          val decode_table = YXML.parse_body #> let open XML.Decode in list (pair string string) end;
    7.13          val decode_list = YXML.parse_body #> let open XML.Decode in list string end;
    7.14        in
    7.15          Resources.init_session_base
    7.16 -          {global_theories = decode_table global_theories_yxml,
    7.17 +          {sessions = decode_list sessions_yxml,
    7.18 +           global_theories = decode_table global_theories_yxml,
    7.19             loaded_theories = decode_list loaded_theories_yxml,
    7.20             known_theories = decode_table known_theories_yxml}
    7.21        end);
     8.1 --- a/src/Pure/PIDE/protocol.scala	Sat Dec 16 20:02:40 2017 +0100
     8.2 +++ b/src/Pure/PIDE/protocol.scala	Sat Dec 16 21:53:07 2017 +0100
     8.3 @@ -341,7 +341,8 @@
     8.4    def session_base(resources: Resources)
     8.5    {
     8.6      val base = resources.session_base.standard_path
     8.7 -    protocol_command("Prover.session_base",
     8.8 +    protocol_command("Prover.init_session_base",
     8.9 +      encode_list(base.known.sessions.toList),
    8.10        encode_table(base.global_theories.toList),
    8.11        encode_list(base.loaded_theories.keys),
    8.12        encode_table(base.dest_known_theories))
     9.1 --- a/src/Pure/PIDE/resources.ML	Sat Dec 16 20:02:40 2017 +0100
     9.2 +++ b/src/Pure/PIDE/resources.ML	Sat Dec 16 21:53:07 2017 +0100
     9.3 @@ -8,13 +8,15 @@
     9.4  sig
     9.5    val default_qualifier: string
     9.6    val init_session_base:
     9.7 -    {global_theories: (string * string) list,
     9.8 +    {sessions: string list,
     9.9 +     global_theories: (string * string) list,
    9.10       loaded_theories: string list,
    9.11       known_theories: (string * string) list} -> unit
    9.12    val finish_session_base: unit -> unit
    9.13    val global_theory: string -> string option
    9.14    val loaded_theory: string -> bool
    9.15    val known_theory: string -> Path.T option
    9.16 +  val check_session: Proof.context -> string * Position.T -> string
    9.17    val master_directory: theory -> Path.T
    9.18    val imports_of: theory -> (string * Position.T) list
    9.19    val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
    9.20 @@ -42,24 +44,27 @@
    9.21  val default_qualifier = "Draft";
    9.22  
    9.23  val empty_session_base =
    9.24 -  {global_theories = Symtab.empty: string Symtab.table,
    9.25 +  {sessions = []: string list,
    9.26 +   global_theories = Symtab.empty: string Symtab.table,
    9.27     loaded_theories = Symtab.empty: unit Symtab.table,
    9.28     known_theories = Symtab.empty: Path.T Symtab.table};
    9.29  
    9.30  val global_session_base =
    9.31    Synchronized.var "Sessions.base" empty_session_base;
    9.32  
    9.33 -fun init_session_base {global_theories, loaded_theories, known_theories} =
    9.34 +fun init_session_base {sessions, global_theories, loaded_theories, known_theories} =
    9.35    Synchronized.change global_session_base
    9.36      (fn _ =>
    9.37 -      {global_theories = Symtab.make global_theories,
    9.38 +      {sessions = sort_strings sessions,
    9.39 +       global_theories = Symtab.make global_theories,
    9.40         loaded_theories = Symtab.make_set loaded_theories,
    9.41         known_theories = Symtab.make (map (apsnd Path.explode) known_theories)});
    9.42  
    9.43  fun finish_session_base () =
    9.44    Synchronized.change global_session_base
    9.45      (fn {global_theories, loaded_theories, ...} =>
    9.46 -      {global_theories = global_theories,
    9.47 +      {sessions = [],
    9.48 +       global_theories = global_theories,
    9.49         loaded_theories = loaded_theories,
    9.50         known_theories = #known_theories empty_session_base});
    9.51  
    9.52 @@ -69,6 +74,21 @@
    9.53  fun loaded_theory a = Symtab.defined (get_session_base #loaded_theories) a;
    9.54  fun known_theory a = Symtab.lookup (get_session_base #known_theories) a;
    9.55  
    9.56 +fun check_session ctxt (name, pos) =
    9.57 +  let val sessions = get_session_base #sessions in
    9.58 +    if member (op =) sessions name then
    9.59 +      (Context_Position.report ctxt pos (Markup.entity Markup.sessionN name); name)
    9.60 +    else
    9.61 +      let
    9.62 +        val completion =
    9.63 +          Completion.make (name, pos) (fn completed =>
    9.64 +              sessions
    9.65 +              |> filter completed
    9.66 +              |> map (fn a => (a, (Markup.sessionN, a))));
    9.67 +        val report = Markup.markup_report (Completion.reported_text completion);
    9.68 +      in error ("Bad session " ^ quote name ^ Position.here pos ^ report) end
    9.69 +  end;
    9.70 +
    9.71  
    9.72  (* manage source files *)
    9.73  
    9.74 @@ -237,7 +257,9 @@
    9.75  in
    9.76  
    9.77  val _ = Theory.setup
    9.78 - (Thy_Output.antiquotation \<^binding>\<open>path\<close> (Scan.lift (Parse.position Parse.path))
    9.79 + (Thy_Output.antiquotation \<^binding>\<open>session\<close> (Scan.lift (Parse.position Parse.embedded))
    9.80 +    (fn {context = ctxt, ...} => Thy_Output.verbatim_text ctxt o check_session ctxt) #>
    9.81 +  Thy_Output.antiquotation \<^binding>\<open>path\<close> (Scan.lift (Parse.position Parse.path))
    9.82      (document_antiq check_path o #context) #>
    9.83    Thy_Output.antiquotation \<^binding>\<open>file\<close> (Scan.lift (Parse.position Parse.path))
    9.84      (document_antiq check_file o #context) #>
    10.1 --- a/src/Pure/Thy/sessions.scala	Sat Dec 16 20:02:40 2017 +0100
    10.2 +++ b/src/Pure/Thy/sessions.scala	Sat Dec 16 21:53:07 2017 +0100
    10.3 @@ -31,6 +31,7 @@
    10.4      val empty: Known = Known()
    10.5  
    10.6      def make(local_dir: Path, bases: List[Base],
    10.7 +      sessions: List[String] = Nil,
    10.8        theories: List[Document.Node.Name] = Nil,
    10.9        loaded_files: List[(String, List[Path])] = Nil): Known =
   10.10      {
   10.11 @@ -46,6 +47,9 @@
   10.12          theories.iterator.filter(name => name.path.canonical_file.toPath.startsWith(local_path))
   10.13        }
   10.14  
   10.15 +      val known_sessions =
   10.16 +        (sessions.toSet /: bases)({ case (known, base) => known ++ base.known.sessions })
   10.17 +
   10.18        val known_theories =
   10.19          (Map.empty[String, Document.Node.Name] /: (bases_iterator(false) ++ theories.iterator))({
   10.20            case (known, name) =>
   10.21 @@ -74,13 +78,16 @@
   10.22        val known_loaded_files =
   10.23          (loaded_files.toMap /: bases.map(base => base.known.loaded_files))(_ ++ _)
   10.24  
   10.25 -      Known(known_theories, known_theories_local,
   10.26 +      Known(
   10.27 +        known_sessions,
   10.28 +        known_theories, known_theories_local,
   10.29          known_files.iterator.map(p => (p._1, p._2.reverse)).toMap,
   10.30          known_loaded_files)
   10.31      }
   10.32    }
   10.33  
   10.34    sealed case class Known(
   10.35 +    sessions: Set[String] = Set.empty,
   10.36      theories: Map[String, Document.Node.Name] = Map.empty,
   10.37      theories_local: Map[String, Document.Node.Name] = Map.empty,
   10.38      files: Map[JFile, List[Document.Node.Name]] = Map.empty,
   10.39 @@ -298,6 +305,7 @@
   10.40  
   10.41              val known =
   10.42                Known.make(info.dir, List(imports_base),
   10.43 +                sessions = List(info.name),
   10.44                  theories = dependencies.theories,
   10.45                  loaded_files = loaded_files)
   10.46  
    11.1 --- a/src/Pure/Tools/build.ML	Sat Dec 16 20:02:40 2017 +0100
    11.2 +++ b/src/Pure/Tools/build.ML	Sat Dec 16 21:53:07 2017 +0100
    11.3 @@ -148,6 +148,7 @@
    11.4    name: string,
    11.5    master_dir: Path.T,
    11.6    theories: (Options.T * (string * Position.T) list) list,
    11.7 +  sessions: string list,
    11.8    global_theories: (string * string) list,
    11.9    loaded_theories: string list,
   11.10    known_theories: (string * string) list};
   11.11 @@ -158,33 +159,34 @@
   11.12      val position = Position.of_properties o properties;
   11.13      val (symbol_codes, (command_timings, (do_output, (verbose, (browser_info,
   11.14        (document_files, (graph_file, (parent_name, (chapter, (name, (master_dir,
   11.15 -      (theories, (global_theories, (loaded_theories, known_theories)))))))))))))) =
   11.16 +      (theories, (sessions, (global_theories, (loaded_theories, known_theories))))))))))))))) =
   11.17        pair (list (pair string int)) (pair (list properties) (pair bool (pair bool (pair string
   11.18          (pair (list (pair string string)) (pair string (pair string (pair string (pair string
   11.19            (pair string
   11.20              (pair (((list (pair Options.decode (list (pair string position))))))
   11.21 -              (pair (list (pair string string))
   11.22 -                (pair (list string) (list (pair string string)))))))))))))))
   11.23 +              (pair (list string) (pair (list (pair string string))
   11.24 +                (pair (list string) (list (pair string string))))))))))))))))
   11.25        (YXML.parse_body yxml);
   11.26    in
   11.27      Args {symbol_codes = symbol_codes, command_timings = command_timings, do_output = do_output,
   11.28        verbose = verbose, browser_info = Path.explode browser_info,
   11.29        document_files = map (apply2 Path.explode) document_files,
   11.30        graph_file = Path.explode graph_file, parent_name = parent_name, chapter = chapter,
   11.31 -      name = name, master_dir = Path.explode master_dir, theories = theories,
   11.32 +      name = name, master_dir = Path.explode master_dir, theories = theories, sessions = sessions,
   11.33        global_theories = global_theories, loaded_theories = loaded_theories,
   11.34        known_theories = known_theories}
   11.35    end;
   11.36  
   11.37  fun build_session (Args {symbol_codes, command_timings, do_output, verbose, browser_info,
   11.38 -    document_files, graph_file, parent_name, chapter, name, master_dir, theories,
   11.39 +    document_files, graph_file, parent_name, chapter, name, master_dir, theories, sessions,
   11.40      global_theories, loaded_theories, known_theories}) =
   11.41    let
   11.42      val symbols = HTML.make_symbols symbol_codes;
   11.43  
   11.44      val _ =
   11.45        Resources.init_session_base
   11.46 -        {global_theories = global_theories,
   11.47 +        {sessions = sessions,
   11.48 +         global_theories = global_theories,
   11.49           loaded_theories = loaded_theories,
   11.50           known_theories = known_theories};
   11.51  
    12.1 --- a/src/Pure/Tools/build.scala	Sat Dec 16 20:02:40 2017 +0100
    12.2 +++ b/src/Pure/Tools/build.scala	Sat Dec 16 21:53:07 2017 +0100
    12.3 @@ -212,14 +212,14 @@
    12.4                  pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
    12.5                  pair(string, pair(string, pair(string, pair(Path.encode,
    12.6                  pair(list(pair(Options.encode, list(pair(string, properties)))),
    12.7 -                pair(list(pair(string, string)), pair(list(string),
    12.8 -                list(pair(string, string))))))))))))))))(
    12.9 +                pair(list(string), pair(list(pair(string, string)), pair(list(string),
   12.10 +                list(pair(string, string)))))))))))))))))(
   12.11                (Symbol.codes, (command_timings, (do_output, (verbose,
   12.12                  (store.browser_info, (info.document_files, (File.standard_path(graph_file),
   12.13                  (parent, (info.chapter, (name, (Path.current,
   12.14 -                (info.theories,
   12.15 +                (info.theories, (base.known.sessions.toList,
   12.16                  (base.global_theories.toList, (base.loaded_theories.keys,
   12.17 -                base.dest_known_theories)))))))))))))))
   12.18 +                base.dest_known_theories))))))))))))))))
   12.19              })
   12.20  
   12.21          val env =