Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Update to Isabelle devleopment version.

This commit is contained in:
Achim D. Brucker 2023-02-19 20:01:01 +00:00
parent f7b4cf67f7
commit de1870fbee
3 changed files with 10 additions and 16 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
Isabelle_DOF-Examples-Extra/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy
View File

@ -1144,8 +1144,7 @@ text\<open>
necessary infrastructure --- i.e. the operations to pack and unpack theories and
queries on it:
\<^item> \<^ML>\<open> Toplevel.theory_toplevel: theory -> Toplevel.state\<close>
\<^item> \<^ML>\<open> Toplevel.init_toplevel: unit -> Toplevel.state\<close>
\<^item> \<^ML>\<open> Toplevel.make_state: theory option -> Toplevel.state\<close>
\<^item> \<^ML>\<open> Toplevel.is_toplevel: Toplevel.state -> bool\<close>
\<^item> \<^ML>\<open> Toplevel.is_theory: Toplevel.state -> bool\<close>
\<^item> \<^ML>\<open> Toplevel.is_proof: Toplevel.state -> bool\<close>
@ -1183,7 +1182,7 @@ text\<open> The extensibility of Isabelle as a system framework depends on a num
\<^item> \<^ML>\<open>Toplevel.theory: (theory -> theory) -> Toplevel.transition -> Toplevel.transition\<close>
adjoins a theory transformer.
\<^item> \<^ML>\<open>Toplevel.generic_theory: (generic_theory -> generic_theory) -> Toplevel.transition -> Toplevel.transition\<close>
\<^item> \<^ML>\<open>Toplevel.theory': (bool -> theory -> theory) -> Toplevel.presentation -> Toplevel.transition -> Toplevel.transition\<close>
\<^item> \<^ML>\<open>Toplevel.theory': (bool -> theory -> theory) -> Toplevel.presentation option -> Toplevel.transition -> Toplevel.transition\<close>
\<^item> \<^ML>\<open>Toplevel.exit: Toplevel.transition -> Toplevel.transition\<close>
\<^item> \<^ML>\<open>Toplevel.ignored: Position.T -> Toplevel.transition\<close>
\<^item> \<^ML>\<open>Toplevel.present_local_theory: (xstring * Position.T) option ->
@ -1201,7 +1200,6 @@ text\<open>
\<^item> \<^ML>\<open>Document.state : unit -> Document.state\<close>, giving the state as a "collection" of named
nodes, each consisting of an editable list of commands, associated with asynchronous
execution process,
\<^item> \<^ML>\<open>Session.get_keywords : unit -> Keyword.keywords\<close>, this looks to be session global,
\<^item> \<^ML>\<open>Thy_Header.get_keywords : theory -> Keyword.keywords\<close> this looks to be just theory global.
@ -1275,7 +1273,6 @@ subsection\<open>Miscellaneous\<close>
text\<open>Here are a few queries relevant for the global config of the isar engine:\<close>
ML\<open> Document.state();\<close>
ML\<open> Session.get_keywords(); (* this looks to be session global. *) \<close>
ML\<open> Thy_Header.get_keywords @{theory};(* this looks to be really theory global. *) \<close>
@ -2153,7 +2150,7 @@ text\<open>
\<^item>\<^ML>\<open>Document_Output.output_document: Proof.context -> {markdown: bool} -> Input.source -> Latex.text \<close>
\<^item>\<^ML>\<open>Document_Output.output_token: Proof.context -> Token.T -> Latex.text \<close>
\<^item>\<^ML>\<open>Document_Output.output_source: Proof.context -> string -> Latex.text \<close>
\<^item>\<^ML>\<open>Document_Output.present_thy: Options.T -> theory -> Document_Output.segment list -> Latex.text \<close>
\<^item>\<^ML>\<open>Document_Output.present_thy: Options.T -> Keyword.keywords -> string -> Document_Output.segment list -> Latex.text \<close>
\<^item>\<^ML>\<open>Document_Output.isabelle: Proof.context -> Latex.text -> Latex.text\<close>
\<^item>\<^ML>\<open>Document_Output.isabelle_typewriter: Proof.context -> Latex.text -> Latex.text\<close>

7
Isabelle_DOF/scala/dof_document_build.scala
View File

@ -42,7 +42,7 @@ object DOF_Document_Build
def the_document_entry(context: Document_Build.Context, name: String): Export.Entry = {
val entries =
for {
node_name <- context.document_theories
node_name <- context.all_document_theories
entry <- context.session_context.get(node_name.theory, name)
} yield entry
@ -60,11 +60,12 @@ object DOF_Document_Build
override def prepare_directory(
context: Document_Build.Context,
dir: Path,
doc: Document_Build.Document_Variant): Document_Build.Directory =
doc: Document_Build.Document_Variant,
verbose: Boolean): Document_Build.Directory =
{
val options = DOF.options(context.options)
val latex_output = new Latex_Output(options)
val directory = context.prepare_directory(dir, doc, latex_output)
val directory = context.prepare_directory(dir, doc, latex_output, verbose)
val isabelle_dof_dir = context.session_context.sessions_structure(DOF.session).dir

10
Isabelle_DOF/thys/Isa_DOF.thy
View File

@ -953,7 +953,7 @@ fun check_path check_file ctxt dir (name, pos) =
val path = Path.append dir (Path.explode name) handle ERROR msg => err msg pos;
val _ = Path.expand path handle ERROR msg => err msg pos;
val _ = Context_Position.report ctxt pos (Markup.path (Path.implode_symbolic path));
val _ = Context_Position.report ctxt pos (Markup.path (File.symbolic_path path));
val _ =
(case check_file of
NONE => path
@ -1857,14 +1857,11 @@ let
fun prin state _ = string_of_term string pos (Toplevel.context_of state)
in
Toplevel.theory(fn thy =>
(print_item prin (string_list, string) (Toplevel.theory_toplevel thy);
(print_item prin (string_list, string) (Toplevel.make_state (SOME thy));
thy |> meta_args_exec meta_args_opt )
) trans
end
val _ = Toplevel.theory
val _ = Toplevel.theory_toplevel
(* setup ontology aware commands *)
@ -2146,7 +2143,7 @@ fun document_command (name, pos) descr mark cmd =
Outer_Syntax.command (name, pos) descr
(ODL_Meta_Args_Parser.attributes -- Parse.document_source >> (fn (meta_args, text) =>
Toplevel.theory' (fn _ => cmd meta_args)
(Toplevel.presentation_context #> document_output_reports name mark meta_args text #> SOME)));
(SOME (Toplevel.presentation_context #> document_output_reports name mark meta_args text))));
(* Core Command Definitions *)
@ -3198,7 +3195,6 @@ ML\<open> (String.concatWith ","); Token.content_of\<close>
ML\<open>
Document.state;
Session.get_keywords();
Parse.command;
Parse.tags;
\<close>