From efe8e7c5077ab3ea5491ebfc70be18a79b7e941d Mon Sep 17 00:00:00 2001 From: bu Date: Thu, 14 Feb 2019 12:03:06 +0100 Subject: [PATCH] changed finbal state error to msg (takes into effect non-strict-checking) --- Isa_DOF.thy | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Isa_DOF.thy b/Isa_DOF.thy index 056f3794..7192eb79 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -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