# HG changeset patch # User wenzelm # Date 1513457587 -3600 # Node ID 81e9804b201482469ae796402b7b840e597e12a4 # Parent e62d72699666c4e70ae433137ce6d9d6148aabea added document antiquotation @{session name}; renamed protocol function "Prover.session_base" to "Prover.init_session_base" according to the ML/Scala operation; diff -r e62d72699666 -r 81e9804b2014 NEWS --- a/NEWS Sat Dec 16 20:02:40 2017 +0100 +++ b/NEWS Sat Dec 16 21:53:07 2017 +0100 @@ -85,6 +85,9 @@ antiquotations in control symbol notation, e.g. \<^const_name> becomes \isactrlconstUNDERSCOREname. +* Document antiquotation @{session name} checks and prints the given +session name verbatim. + * Document preparation with skip_proofs option now preserves the content more accurately: only terminal proof steps ('by' etc.) are skipped. diff -r e62d72699666 -r 81e9804b2014 src/Doc/Isar_Ref/Document_Preparation.thy --- a/src/Doc/Isar_Ref/Document_Preparation.thy Sat Dec 16 20:02:40 2017 +0100 +++ b/src/Doc/Isar_Ref/Document_Preparation.thy Sat Dec 16 21:53:07 2017 +0100 @@ -107,6 +107,7 @@ @{antiquotation_def emph} & : & \antiquotation\ \\ @{antiquotation_def bold} & : & \antiquotation\ \\ @{antiquotation_def verbatim} & : & \antiquotation\ \\ + @{antiquotation_def session} & : & \antiquotation\ \\ @{antiquotation_def "file"} & : & \antiquotation\ \\ @{antiquotation_def "url"} & : & \antiquotation\ \\ @{antiquotation_def "cite"} & : & \antiquotation\ \\ @@ -195,6 +196,7 @@ @@{antiquotation emph} options @{syntax text} | @@{antiquotation bold} options @{syntax text} | @@{antiquotation verbatim} options @{syntax text} | + @@{antiquotation session} options @{syntax embedded} | @@{antiquotation path} options @{syntax embedded} | @@{antiquotation "file"} options @{syntax name} | @@{antiquotation dir} options @{syntax name} | @@ -284,6 +286,9 @@ \<^descr> \@{verbatim s}\ prints uninterpreted source text literally as ASCII characters, using some type-writer font style. + \<^descr> \@{session name}\ prints given session name verbatim. The name is checked + wrt.\ the dependencies of the current session. + \<^descr> \@{path name}\ prints the file-system path name verbatim. \<^descr> \@{file name}\ is like \@{path name}\, but ensures that \name\ refers to a diff -r e62d72699666 -r 81e9804b2014 src/Doc/ROOT --- a/src/Doc/ROOT Sat Dec 16 20:02:40 2017 +0100 +++ b/src/Doc/ROOT Sat Dec 16 21:53:07 2017 +0100 @@ -372,6 +372,8 @@ session System (doc) in "System" = Pure + options [document_variants = "system", thy_output_source] + sessions + "HOL-Library" theories Environment Sessions diff -r e62d72699666 -r 81e9804b2014 src/Doc/System/Presentation.thy --- a/src/Doc/System/Presentation.thy Sat Dec 16 20:02:40 2017 +0100 +++ b/src/Doc/System/Presentation.thy Sat Dec 16 21:53:07 2017 +0100 @@ -69,9 +69,9 @@ The presentation output will appear in \<^verbatim>\$ISABELLE_BROWSER_INFO/FOL/FOL\ as reported by the above verbose invocation of the build process. - Many Isabelle sessions (such as \<^verbatim>\HOL-Library\ in \<^dir>\~~/src/HOL/Library\) - also provide printable documents in PDF. These are prepared automatically as - well if enabled like this: + Many Isabelle sessions (such as \<^session>\HOL-Library\ in + \<^dir>\~~/src/HOL/Library\) also provide printable documents in PDF. These are + prepared automatically as well if enabled like this: @{verbatim [display] \isabelle build -o browser_info -o document=pdf -v -c HOL-Library\} Enabling both browser info and document preparation simultaneously causes an diff -r e62d72699666 -r 81e9804b2014 src/Pure/ML/ml_process.scala --- a/src/Pure/ML/ml_process.scala Sat Dec 16 20:02:40 2017 +0100 +++ b/src/Pure/ML/ml_process.scala Sat Dec 16 21:53:07 2017 +0100 @@ -102,7 +102,8 @@ def print_list(list: List[String]): String = ML_Syntax.print_list(ML_Syntax.print_string_bytes)(list) List("Resources.init_session_base" + - " {global_theories = " + print_table(base.global_theories.toList) + + " {sessions = " + print_list(base.known.sessions.toList) + + ", global_theories = " + print_table(base.global_theories.toList) + ", loaded_theories = " + print_list(base.loaded_theories.keys) + ", known_theories = " + print_table(base.dest_known_theories) + "}") } diff -r e62d72699666 -r 81e9804b2014 src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Sat Dec 16 20:02:40 2017 +0100 +++ b/src/Pure/PIDE/markup.ML Sat Dec 16 21:53:07 2017 +0100 @@ -72,6 +72,7 @@ val wordsN: string val words: T val hiddenN: string val hidden: T val system_optionN: string + val sessionN: string val theoryN: string val classN: string val type_nameN: string @@ -394,6 +395,8 @@ val system_optionN = "system_option"; +val sessionN = "session"; + val theoryN = "theory"; val classN = "class"; val type_nameN = "type_name"; diff -r e62d72699666 -r 81e9804b2014 src/Pure/PIDE/protocol.ML --- a/src/Pure/PIDE/protocol.ML Sat Dec 16 20:02:40 2017 +0100 +++ b/src/Pure/PIDE/protocol.ML Sat Dec 16 21:53:07 2017 +0100 @@ -18,14 +18,15 @@ Isabelle_Process.init_options_interactive ())); val _ = - Isabelle_Process.protocol_command "Prover.session_base" - (fn [global_theories_yxml, loaded_theories_yxml, known_theories_yxml] => + Isabelle_Process.protocol_command "Prover.init_session_base" + (fn [sessions_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 - {global_theories = decode_table global_theories_yxml, + {sessions = decode_list sessions_yxml, + global_theories = decode_table global_theories_yxml, loaded_theories = decode_list loaded_theories_yxml, known_theories = decode_table known_theories_yxml} end); diff -r e62d72699666 -r 81e9804b2014 src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Sat Dec 16 20:02:40 2017 +0100 +++ b/src/Pure/PIDE/protocol.scala Sat Dec 16 21:53:07 2017 +0100 @@ -341,7 +341,8 @@ def session_base(resources: Resources) { val base = resources.session_base.standard_path - protocol_command("Prover.session_base", + protocol_command("Prover.init_session_base", + encode_list(base.known.sessions.toList), encode_table(base.global_theories.toList), encode_list(base.loaded_theories.keys), encode_table(base.dest_known_theories)) diff -r e62d72699666 -r 81e9804b2014 src/Pure/PIDE/resources.ML --- a/src/Pure/PIDE/resources.ML Sat Dec 16 20:02:40 2017 +0100 +++ b/src/Pure/PIDE/resources.ML Sat Dec 16 21:53:07 2017 +0100 @@ -8,13 +8,15 @@ sig val default_qualifier: string val init_session_base: - {global_theories: (string * string) list, + {sessions: string list, + global_theories: (string * string) list, loaded_theories: string list, known_theories: (string * string) list} -> unit val finish_session_base: unit -> unit val global_theory: string -> string option val loaded_theory: string -> bool val known_theory: string -> Path.T option + val check_session: 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 @@ -42,24 +44,27 @@ val default_qualifier = "Draft"; val empty_session_base = - {global_theories = Symtab.empty: string Symtab.table, + {sessions = []: string list, + global_theories = Symtab.empty: string Symtab.table, loaded_theories = Symtab.empty: unit Symtab.table, known_theories = Symtab.empty: Path.T Symtab.table}; val global_session_base = Synchronized.var "Sessions.base" empty_session_base; -fun init_session_base {global_theories, loaded_theories, known_theories} = +fun init_session_base {sessions, global_theories, loaded_theories, known_theories} = Synchronized.change global_session_base (fn _ => - {global_theories = Symtab.make global_theories, + {sessions = sort_strings sessions, + global_theories = Symtab.make global_theories, loaded_theories = Symtab.make_set loaded_theories, known_theories = Symtab.make (map (apsnd Path.explode) known_theories)}); fun finish_session_base () = Synchronized.change global_session_base (fn {global_theories, loaded_theories, ...} => - {global_theories = global_theories, + {sessions = [], + global_theories = global_theories, loaded_theories = loaded_theories, known_theories = #known_theories empty_session_base}); @@ -69,6 +74,21 @@ 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) + else + let + val completion = + Completion.make (name, pos) (fn completed => + sessions + |> filter completed + |> map (fn a => (a, (Markup.sessionN, a)))); + val report = Markup.markup_report (Completion.reported_text completion); + in error ("Bad session " ^ quote name ^ Position.here pos ^ report) end + end; + (* manage source files *) @@ -237,7 +257,9 @@ in val _ = Theory.setup - (Thy_Output.antiquotation \<^binding>\path\ (Scan.lift (Parse.position Parse.path)) + (Thy_Output.antiquotation \<^binding>\session\ (Scan.lift (Parse.position Parse.embedded)) + (fn {context = ctxt, ...} => Thy_Output.verbatim_text ctxt o check_session ctxt) #> + Thy_Output.antiquotation \<^binding>\path\ (Scan.lift (Parse.position Parse.path)) (document_antiq check_path o #context) #> Thy_Output.antiquotation \<^binding>\file\ (Scan.lift (Parse.position Parse.path)) (document_antiq check_file o #context) #> diff -r e62d72699666 -r 81e9804b2014 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Sat Dec 16 20:02:40 2017 +0100 +++ b/src/Pure/Thy/sessions.scala Sat Dec 16 21:53:07 2017 +0100 @@ -31,6 +31,7 @@ val empty: Known = Known() def make(local_dir: Path, bases: List[Base], + sessions: List[String] = Nil, theories: List[Document.Node.Name] = Nil, loaded_files: List[(String, List[Path])] = Nil): Known = { @@ -46,6 +47,9 @@ theories.iterator.filter(name => name.path.canonical_file.toPath.startsWith(local_path)) } + val known_sessions = + (sessions.toSet /: bases)({ case (known, base) => known ++ base.known.sessions }) + val known_theories = (Map.empty[String, Document.Node.Name] /: (bases_iterator(false) ++ theories.iterator))({ case (known, name) => @@ -74,13 +78,16 @@ val known_loaded_files = (loaded_files.toMap /: bases.map(base => base.known.loaded_files))(_ ++ _) - Known(known_theories, known_theories_local, + Known( + known_sessions, + known_theories, known_theories_local, known_files.iterator.map(p => (p._1, p._2.reverse)).toMap, known_loaded_files) } } sealed case class Known( + sessions: Set[String] = Set.empty, theories: Map[String, Document.Node.Name] = Map.empty, theories_local: Map[String, Document.Node.Name] = Map.empty, files: Map[JFile, List[Document.Node.Name]] = Map.empty, @@ -298,6 +305,7 @@ val known = Known.make(info.dir, List(imports_base), + sessions = List(info.name), theories = dependencies.theories, loaded_files = loaded_files) diff -r e62d72699666 -r 81e9804b2014 src/Pure/Tools/build.ML --- a/src/Pure/Tools/build.ML Sat Dec 16 20:02:40 2017 +0100 +++ b/src/Pure/Tools/build.ML Sat Dec 16 21:53:07 2017 +0100 @@ -148,6 +148,7 @@ name: string, master_dir: Path.T, theories: (Options.T * (string * Position.T) list) list, + sessions: string list, global_theories: (string * string) list, loaded_theories: string list, known_theories: (string * string) list}; @@ -158,33 +159,34 @@ 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, (global_theories, (loaded_theories, known_theories)))))))))))))) = + (theories, (sessions, (global_theories, (loaded_theories, known_theories))))))))))))))) = 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 (pair string string)) - (pair (list string) (list (pair string string))))))))))))))) + (pair (list string) (pair (list (pair string string)) + (pair (list string) (list (pair string string)))))))))))))))) (YXML.parse_body yxml); in Args {symbol_codes = symbol_codes, command_timings = command_timings, do_output = do_output, verbose = verbose, browser_info = Path.explode browser_info, 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, + name = name, master_dir = Path.explode master_dir, theories = theories, sessions = sessions, global_theories = global_theories, loaded_theories = loaded_theories, known_theories = known_theories} 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, + document_files, graph_file, parent_name, chapter, name, master_dir, theories, sessions, global_theories, loaded_theories, known_theories}) = let val symbols = HTML.make_symbols symbol_codes; val _ = Resources.init_session_base - {global_theories = global_theories, + {sessions = sessions, + global_theories = global_theories, loaded_theories = loaded_theories, known_theories = known_theories}; diff -r e62d72699666 -r 81e9804b2014 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Sat Dec 16 20:02:40 2017 +0100 +++ b/src/Pure/Tools/build.scala Sat Dec 16 21:53:07 2017 +0100 @@ -212,14 +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(pair(string, string)), pair(list(string), - list(pair(string, string))))))))))))))))( + pair(list(string), pair(list(pair(string, string)), pair(list(string), + list(pair(string, 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, + (info.theories, (base.known.sessions.toList, (base.global_theories.toList, (base.loaded_theories.keys, - base.dest_known_theories))))))))))))))) + base.dest_known_theories)))))))))))))))) }) val env =