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

- Fixed the FrontEnd - level problem according to what we discussed: 

-- there are classes that do not have a level
-- title, subtitle and abstract DO NOT HAVE a level
-- text* has a level, but the level "None"

- Tested whatever we have as examples
This commit is contained in:
Burkhart Wolff 2018-12-04 10:41:34 +01:00
parent 17c66f0fea
commit 5e7ac1c02e
5 changed files with 47 additions and 33 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
Isa_COL.thy
View File

@ -29,7 +29,6 @@ doc_class side_by_side_figure = figure +
caption2 :: "string"
ML\<open>DOF_core.SPY;\<close>
doc_class figure_group =
(* trace :: "doc_class rexp list" <= "[]" automatically generated since monitor clause *)
anchor :: "string"
@ -37,13 +36,22 @@ doc_class figure_group =
rejects figure_group (* this forbids recursive figure-groups *)
accepts "\<lbrace>figure\<rbrace>\<^sup>+"
ML\<open>@{term "side_by_side_figure"};
@{typ "doc_class rexp"};
DOF_core.SPY;
\<close>
(* dito the future table *)
(* dito the future monitor: table - block *)
section\<open>Tests\<close>
ML\<open>@{term "side_by_side_figure"};
@{typ "doc_class rexp"};
DOF_core.SPY;
\<close>
end

48
Isa_DOF.thy
View File

@ -122,7 +122,7 @@ struct
type ISA_transformer_tab = (theory -> term * typ * Position.T -> term option) Symtab.table
val initial_ISA_tab:ISA_transformer_tab = Symtab.empty
type docclass_inv_tab = (string -> Context.generic -> bool) Symtab.table
type docclass_inv_tab = (string -> {is_monitor:bool} -> Context.generic -> bool) Symtab.table
val initial_docclass_inv_tab : docclass_inv_tab = Symtab.empty
type open_monitor_info = {accepted_cids : string list,
@ -285,7 +285,7 @@ fun update_class_invariant cid_long f thy =
let val _ = if is_defined_cid_global' cid_long thy then ()
else error("undefined class id : " ^cid_long)
in map_data_global (upd_docclass_inv_tab (Symtab.update (cid_long,
(fn ctxt => ((writeln("Inv check of :" ^cid_long); f ctxt ))))))
(fn ctxt => ((writeln("Inv check of : " ^cid_long); f ctxt ))))))
thy
end
@ -294,7 +294,7 @@ fun get_class_invariant cid_long thy =
else error("undefined class id : " ^cid_long)
val {docclass_inv_tab, ...} = get_data_global thy
in case Symtab.lookup docclass_inv_tab cid_long of
NONE => K(K true)
NONE => K(K(K true))
| SOME f => f
end
@ -1008,7 +1008,8 @@ fun create_and_check_docitem is_monitor oid pos cid_pos doc_attrs thy =
fun conv_attrs ((lhs, pos), rhs) = (markup2string lhs,pos,"=", Syntax.read_term_global thy rhs)
val assns' = map conv_attrs doc_attrs
val (value_term, _(*ty*), _) = calc_update_term thy cid_long assns' defaults
val check_inv = (DOF_core.get_class_invariant cid_long thy oid) o Context.Theory
val check_inv = (DOF_core.get_class_invariant cid_long thy oid {is_monitor=is_monitor})
o Context.Theory
in thy |> DOF_core.define_object_global (oid, {pos = pos,
thy_name = Context.theory_name thy,
value = value_term,
@ -1040,20 +1041,26 @@ fun update_instance_command (((oid:string,pos),cid_pos),
Syntax.read_term_global thy rhs)
val assns' = map conv_attrs doc_attrs
val def_trans = #1 o (calc_update_term thy cid_long assns')
val check_inv = (DOF_core.get_class_invariant cid_long thy oid) o Context.Theory
val check_inv = (DOF_core.get_class_invariant cid_long thy oid {is_monitor=false})
o Context.Theory
in
thy |> DOF_core.update_value_global oid (def_trans)
|> (fn thy => (check_inv thy; thy))
end
fun enriched_document_command markdown (((((oid,pos),cid_pos), doc_attrs) : meta_args_t,
fun enriched_document_command markdown level (((((oid,pos),cid_pos), doc_attrs) : meta_args_t,
xstring_opt:(xstring * Position.T) option),
toks:Input.source)
: Toplevel.transition -> Toplevel.transition =
let
fun check_text thy = (Thy_Output.output_text(Toplevel.theory_toplevel thy) markdown toks; thy)
(* as side-effect, generates markup *)
fun check_text thy = (Thy_Output.output_text(Toplevel.theory_toplevel thy) markdown toks; thy)
(* generating the level-attribute syntax *)
val doc_attrs' = case level of
NONE => doc_attrs
| SOME(NONE) => (("level",@{here}),"None")::doc_attrs
| SOME(SOME x) => (("level",@{here}),"Some("^ Int.toString x ^"::int)")::doc_attrs
in
Toplevel.theory(create_and_check_docitem false oid pos cid_pos doc_attrs #> check_text)
(* Thanks Frederic Tuong! ! ! *)
@ -1091,7 +1098,8 @@ fun close_monitor_command (args as (((oid:string,pos),cid_pos),
| NONE => error ("Not belonging to a monitor class: "^oid)
val delete_monitor_entry = DOF_core.map_data_global (DOF_core.upd_monitor_tabs (Symtab.delete oid))
val {cid=cid_long, ...} = the(DOF_core.get_object_global oid thy)
val check_inv = (DOF_core.get_class_invariant cid_long thy oid) o Context.Theory
val check_inv = (DOF_core.get_class_invariant cid_long thy oid) {is_monitor=true}
o Context.Theory
in thy |> update_instance_command args
|> (fn thy => (check_inv thy; thy))
|> delete_monitor_entry
@ -1101,59 +1109,59 @@ fun close_monitor_command (args as (((oid:string,pos),cid_pos),
val _ =
Outer_Syntax.command ("title*", @{here}) "section heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> enriched_document_command {markdown = false});
>> enriched_document_command {markdown = false} NONE) ;
val _ =
Outer_Syntax.command ("subtitle*", @{here}) "section heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> enriched_document_command {markdown = false});
>> enriched_document_command {markdown = false} NONE);
val _ =
Outer_Syntax.command ("chapter*", @{here}) "section heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> enriched_document_command {markdown = false});
>> enriched_document_command {markdown = false} (SOME(SOME 0)));
val _ =
Outer_Syntax.command ("section*", @{here}) "section heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> enriched_document_command {markdown = false});
>> enriched_document_command {markdown = false} (SOME(SOME 1)));
val _ =
Outer_Syntax.command ("subsection*", @{here}) "subsection heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> enriched_document_command {markdown = false});
>> enriched_document_command {markdown = false} (SOME(SOME 2)));
val _ =
Outer_Syntax.command ("subsubsection*", @{here}) "subsubsection heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> enriched_document_command {markdown = false});
>> enriched_document_command {markdown = false} (SOME(SOME 3)));
val _ =
Outer_Syntax.command ("paragraph*", @{here}) "paragraph heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> enriched_document_command {markdown = false});
>> enriched_document_command {markdown = false} (SOME(SOME 4)));
val _ =
Outer_Syntax.command ("subparagraph*", @{here}) "subparagraph heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> enriched_document_command {markdown = false});
>> enriched_document_command {markdown = false} (SOME(SOME 5)));
val _ =
Outer_Syntax.command ("figure*", @{here}) "figure"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> enriched_document_command {markdown = false});
>> enriched_document_command {markdown = false} NONE);
val _ =
Outer_Syntax.command ("side_by_side_figure*", @{here}) "multiple figures"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> enriched_document_command {markdown = false});
>> enriched_document_command {markdown = false} NONE);
val _ =
Outer_Syntax.command ("text*", @{here}) "formal comment (primary style)"
(attributes -- Parse.opt_target -- Parse.document_source
>> enriched_document_command {markdown = true});
>> enriched_document_command {markdown = true} (SOME NONE));
val _ =
Outer_Syntax.command @{command_keyword "declare_reference*"}
@ -1537,6 +1545,4 @@ writeln (DOF_core.toStringDocItemRef "scholarly_paper.introduction" "XX" []);
\<close>
*)
end

2
examples/conceptual/Concept_ExampleInvariant.thy
View File

@ -91,7 +91,7 @@ text*[c2::C, x = "''delta''"] \<open> ... in ut tortor eleifend augue pretium co
section*[f::E] \<open> Lectus accumsan velit ultrices, ... }\<close>
(* test : close_monitor should fail : *
(* test : close_monitor should fail :
section*[f2::E] \<open> Lectus accumsan velit ultrices, ... }\<close>
*)
ML\<open>val term = AttributeAccess.calc_attr_access (Context.Proof @{context}) "trace" "struct" @{here};

2
examples/math_exam/BAC2017/BAC2017.thy
View File

@ -86,7 +86,7 @@ lemma q2_b : "0 \<le> x \<and> x \<le> y \<and> y \<le> 1 \<Longrightarrow> h x
lemma q2_c : "1 \<le> x \<and> x \<le> y \<Longrightarrow> h x \<ge> h y"
sorry
text*[v2::Validation, proofs="[@{thm ''q2_b''}, @{thm ''q2_c''}]"]
text*[v2::Validation, proofs="[@{thm ''BAC2017.q2_b''}, @{thm ''BAC2017.q2_c''}]"]
{* See lemmas @{thm q2_b} and @{thm q2_c}. *}

10
examples/scholarly_paper/2018_cicm/IsaDofApplications.thy
View File

@ -44,8 +44,8 @@ on top of Isabelle. \isadof allows for conventional typesetting
for enforcing a certain document structure, and discuss ontology-specific IDE support.
\<close>
section*[intro::introduction_title]\<open> Introduction \<close>
text*[introtext::introduction_elem]\<open>
section*[intro::introduction]\<open> Introduction \<close>
text*[introtext::introduction]\<open>
The linking of the \<^emph>\<open>formal\<close> to the \<^emph>\<open>informal\<close> is perhaps the
most pervasive challenge in the digitization of knowledge and its
propagation. This challenge incites numerous research efforts
@ -94,7 +94,7 @@ declare_reference*[ontomod::text_section]
declare_reference*[ontopide::text_section]
declare_reference*[conclusion::text_section]
(*>*)
text*[plan::introduction_elem]\<open> The plan of the paper is follows: we start by introducing the underlying
text*[plan::introduction]\<open> The plan of the paper is follows: we start by introducing the underlying
Isabelel sytem (@{docitem (unchecked) \<open>bgrnd\<close>}) followed by presenting the
essentials of \isadof and its ontology language (@{docitem (unchecked) \<open>isadof\<close>}).
It follows @{docitem (unchecked) \<open>ontomod\<close>}, where we present three application
@ -104,7 +104,7 @@ conclusions and discuss related work in @{docitem_ref (unchecked) \<open>conclu
section*[bgrnd::text_section,main_author="Some(@{docitem ''adb''}::author)"]
\<open> Background: The Isabelle System \<close>
text*[background::introduction_elem]\<open>
text*[background::introduction]\<open>
While Isabelle is widely perceived as an interactive theorem prover
for HOL (Higher-order Logic)~@{cite "nipkow.ea:isabelle:2002"}, we
would like to emphasize the view that Isabelle is far more than that:
@ -133,7 +133,7 @@ figure*[architecture::figure,relative_width="100",src="''figures/isabelle-archit
asynchronous communication between the Isabelle system and
the IDE (right-hand side). \<close>
text*[blug::introduction_elem]\<open> The Isabelle system architecture shown in @{docitem_ref \<open>architecture\<close>}
text*[blug::introduction]\<open> The Isabelle system architecture shown in @{docitem_ref \<open>architecture\<close>}
comes with many layers, with Standard ML (SML) at the bottom layer as implementation
language. The architecture actually foresees a \<^emph>\<open>Nano-Kernel\<close> (our terminology) which
resides in the SML structure \texttt{Context}. This structure provides a kind of container called