# HG changeset patch # User aspinall # Date 1168341120 -3600 # Node ID 64f8f5433f3078e01975118a86dbf1a780c7634a # Parent c874c3f13c454c8069702764575627fff254b865 Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag. diff -r c874c3f13c45 -r 64f8f5433f30 src/Pure/ProofGeneral/proof_general_pgip.ML --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Tue Jan 09 12:09:49 2007 +0100 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Tue Jan 09 12:12:00 2007 +0100 @@ -13,6 +13,10 @@ (* These two are just to support the semi-PGIP Emacs mode *) val init_pgip_channel: (string -> unit) -> unit val process_pgip: string -> unit + + (* Yet more message functions... *) + val nonfatal_error : string -> unit (* recoverable error *) + val log_msg : string -> unit (* for internal log messages *) end structure ProofGeneralPgip : PROOF_GENERAL_PGIP = @@ -170,6 +174,7 @@ delayed_msgs := pgip :: ! delayed_msgs else issue_pgip pgip in + (* Normal responses are messages for the user *) fun normalmsg area cat urgent s = let val content = XML.Elem("pgmltext",[],[XML.Rawtext s]) @@ -179,6 +184,7 @@ queue_or_issue pgip end + (* Error responses are error messages for the user, or system-level messages *) fun errormsg fatality s = let val content = XML.Elem("pgmltext",[],[XML.Rawtext s]) @@ -198,24 +204,38 @@ FIXME: this may cause us problems now we're generating trees; on the other hand the output functions were tuned some time ago, so it ought to be enough to use Rawtext always above. *) +(* NB 2: all of standard functions print strings terminated with new lines, but we don't + add new lines explicitly in PGIP: they are left implicit. It means that PGIP messages + can't be written without newlines. *) fun setup_messages () = (writeln_fn := (fn s => normalmsg Message Normal false s); priority_fn := (fn s => normalmsg Message Normal true s); tracing_fn := (fn s => normalmsg Message Tracing false s); - info_fn := (fn s => normalmsg Message Information false s); - debug_fn := (fn s => normalmsg Message Internal false s); + info_fn := (fn s => errormsg Info s); warning_fn := (fn s => errormsg Warning s); error_fn := (fn s => errormsg Fatal s); - panic_fn := (fn s => errormsg Panic s)); + panic_fn := (fn s => errormsg Panic s); + debug_fn := (fn s => errormsg Debug s)); + +fun nonfatal_error s = errormsg Nonfatal s; +fun log_msg s = errormsg Log s; (* immediate messages *) fun tell_clear_goals () = issue_pgip (Cleardisplay {area=Display}) fun tell_clear_response () = issue_pgip (Cleardisplay {area=Message}) -fun tell_file_loaded path = issue_pgip (Informfileloaded {url=PgipTypes.pgipurl_of_path path}) -fun tell_file_retracted path = issue_pgip (Informfileretracted {url=PgipTypes.pgipurl_of_path path}) + +fun tell_file_loaded completed path = + issue_pgip (Informfileloaded {url=PgipTypes.pgipurl_of_path path, + completed=completed}) +fun tell_file_outdated completed path = + issue_pgip (Informfileoutdated {url=PgipTypes.pgipurl_of_path path, + completed=completed}) +fun tell_file_retracted completed path = + issue_pgip (Informfileretracted {url=PgipTypes.pgipurl_of_path path, + completed=completed}) @@ -254,13 +274,23 @@ (* theory loader actions *) local - + (* da: TODO: PGIP has a completed flag so the prover can indicate to the + interface which files are busy performing a particular action. + To make use of this we need to adjust the hook in thy_info.ML + (may actually be difficult to tell the interface *which* action is in + progress, but we could add a generic "Lock" action which uses + informfileloaded: the broker/UI should not infer too much from incomplete + operations). + *) fun trace_action action name = if action = ThyInfo.Update then - List.app tell_file_loaded (ThyInfo.loaded_files name) - else if action = ThyInfo.Outdate orelse action = ThyInfo.Remove then - List.app tell_file_retracted (ThyInfo.loaded_files name) - else (); + List.app (tell_file_loaded true) (ThyInfo.loaded_files name) + else if action = ThyInfo.Outdate then + List.app (tell_file_outdated true) (ThyInfo.loaded_files name) + else if action = ThyInfo.Remove then + List.app (tell_file_retracted true) (ThyInfo.loaded_files name) + else () + in fun setup_thy_loader () = ThyInfo.add_hook trace_action; @@ -270,18 +300,18 @@ (* get informed about files *) -val thy_name = Path.implode o #1 o Path.split_ext o Path.base o Path.explode; +val thy_name = Path.implode o #1 o Path.split_ext o Path.base; val inform_file_retracted = ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name; val inform_file_processed = ThyInfo.if_known_thy ThyInfo.touch_child_thys o thy_name; -fun proper_inform_file_processed file state = - let val name = thy_name file in +fun proper_inform_file_processed path state = + let val name = thy_name path in if Toplevel.is_toplevel state andalso ThyInfo.known_thy name then (ThyInfo.touch_child_thys name; ThyInfo.pretend_use_thy_only name handle ERROR msg => (warning msg; warning ("Failed to register theory: " ^ quote name); - tell_file_retracted (Path.base (Path.explode file)))) + tell_file_retracted true (Path.base path))) else raise Toplevel.UNDEF end; @@ -739,8 +769,7 @@ fun closefile vs = case !currently_open_file of - SOME f => (proper_inform_file_processed (File.platform_path f) - (Isar.state()); + SOME f => (proper_inform_file_processed f (Isar.state()); priority ("Finished working in file: " ^ PgipTypes.string_of_pgipurl f); currently_open_file := NONE) | NONE => raise PGIP (" when no file is open!") @@ -770,7 +799,11 @@ case !currently_open_file of SOME f => raise PGIP (" when a file is open!") | NONE => (priority ("Retracting file: " ^ PgipTypes.string_of_pgipurl url); - inform_file_retracted (File.platform_path url)) + (* TODO: next should be in thy loader, here just for testing *) + let + val name = thy_name url + in List.app (tell_file_retracted false) (ThyInfo.loaded_files name) end; + inform_file_retracted url) end