nicolas.meric
/
Isabelle_DOF
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

changed finbal state error to msg (takes into effect non-strict-checking)

This commit is contained in:
Burkhart Wolff 2019-02-14 12:03:06 +01:00
parent dec5c9bf86
commit efe8e7c507
1 changed files with 2 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
Isa_DOF.thy
View File

@ -1139,7 +1139,8 @@ fun close_monitor_command (args as (((oid:string,pos),cid_pos),
let val {monitor_tab,...} = DOF_core.get_data_global thy
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.")
then msg thy ("monitor number "^Int.toString i^
" not in final state.")
else ()
end
val _ = case Symtab.lookup monitor_tab oid of