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

Added finality check on monitor closes and check for open monitors in the global check.

This commit is contained in:
Burkhart Wolff 2018-12-10 14:15:39 +01:00
parent d97313d010
commit 40c12801c6
3 changed files with 21 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
Isa_COL.thy
View File

@ -34,7 +34,8 @@ doc_class side_by_side_figure = figure +
doc_class figure_group =
(* trace :: "doc_class rexp list" <= "[]" automatically generated since monitor clause *)
caption :: "string"
rejects figure_group (* this forbids recursive figure-groups *)
rejects figure_group (* this forbids recursive figure-groups not supported
by the current LaTeX style-file. *)
accepts "\<lbrace>figure\<rbrace>\<^sup>+"

30
Isa_DOF.thy
View File

@ -564,11 +564,15 @@ fun print_doc_classes b ctxt =
end;
fun check_doc_global (strict_checking : bool) ctxt =
let val {docobj_tab={tab = x, ...}, ...} = get_data ctxt;
let val {docobj_tab={tab = x, ...}, monitor_tab, ...} = get_data ctxt;
val S = map_filter (fn (s,NONE) => SOME s | _ => NONE) (Symtab.dest x)
val T = map fst (Symtab.dest monitor_tab)
in if null S
then ()
else error("Global consistency error - Unresolved forward references: "^ String.concatWith "," S)
then if null T then ()
else error("Global consistency error - there are open monitors: "
^ String.concatWith "," T)
else error("Global consistency error - Unresolved forward references: "
^ String.concatWith "," S)
end
val _ =
@ -1113,9 +1117,13 @@ fun open_monitor_command ((((oid,pos),cid_pos), doc_attrs) : meta_args_t) =
fun close_monitor_command (args as (((oid:string,pos),cid_pos),
doc_attrs: (((string*Position.T)*string)*string)list)) thy =
let val {monitor_tab,...} = DOF_core.get_data_global thy
fun check_if_final {accepted_cids, rejected_cids,automatas} = true (* check if final: TODO *)
fun check_if_final aS = let val i = find_index (not o RegExpInterface.final) aS
in if i >= 0
then error("monitor number "^ Int.toString i^" not in final state.")
else ()
end
val _ = case Symtab.lookup monitor_tab oid of
SOME X => check_if_final X
SOME {automatas,...} => check_if_final automatas
| 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)
@ -1198,15 +1206,13 @@ val _ =
val _ =
Outer_Syntax.command @{command_keyword "close_monitor*"}
"close a document reference monitor"
(attributes_upd >> (fn args => Toplevel.theory(close_monitor_command args)));
(attributes_upd >> (Toplevel.theory o close_monitor_command));
val update_instance_command' = Toplevel.theory o update_instance_command
val _ =
Outer_Syntax.command @{command_keyword "update_instance*"}
"update meta-attributes of an instance of a document class"
(attributes_upd >> update_instance_command');
(attributes_upd >> (Toplevel.theory o update_instance_command));
(* dummy/fake so far: *)
val update_lemma_cmd = (fn (((oid,pos),cid),doc_attrs) => (Toplevel.theory (I)))
@ -1263,9 +1269,9 @@ fun theorem spec schematic descr =
val _ = theorem @{command_keyword "theorem*"} false "theorem";
(* val _ = theorem @{command_keyword "lemma*"} false "lemma";
val _ = theorem @{command_keyword corollary} false "corollary";
val _ = theorem @{command_keyword proposition} false "proposition";
val _ = theorem @{command_keyword schematic_goal} true "schematic goal"; *)
val _ = theorem @{command_keyword corollary} false "corollary";
val _ = theorem @{command_keyword proposition} false "proposition";
val _ = theorem @{command_keyword schematic_goal} true "schematic goal"; *)
in end\<close>

2
examples/conceptual/Concept_ExampleInvariant.thy
View File

@ -93,7 +93,7 @@ section*[f::E] \<open> Lectus accumsan velit ultrices, ... }\<clo
section*[f2::E] \<open> Lectus accumsan velit ultrices, ... }\<close>
*)
ML\<open>val term = AttributeAccess.calc_attr_access (Context.Proof @{context}) "trace" "struct" @{here} @{here} ;
ML\<open>val term = AttributeAccess.compute_attr_access (Context.Proof @{context}) "trace" "struct" @{here} @{here} ;
fun conv (Const(@{const_name "Pair"},_) $ Const(s,_) $ S) = (s, HOLogic.dest_string S)
val string_pair_list = map conv (HOLogic.dest_list term)
\<close>