Path.split_ext; more robust inform_file_processed;
authorwenzelm
Wed Jun 09 18:54:07 2004 +0200 (2004-06-09)
changeset 14902bef0dc694c48
parent 14901 c7a8a8eb7fc8
child 14903 d264b8ad3eec
Path.split_ext; more robust inform_file_processed;
src/Pure/proof_general.ML
     1.1 --- a/src/Pure/proof_general.ML	Wed Jun 09 18:53:41 2004 +0200
     1.2 +++ b/src/Pure/proof_general.ML	Wed Jun 09 18:54:07 2004 +0200
     1.3 @@ -134,6 +134,7 @@
     1.4  fun tell_clear_goals () = notify "Proof General, please clear the goals buffer.";
     1.5  fun tell_clear_response () = notify "Proof General, please clear the response buffer.";
     1.6  fun tell_file msg path = notify ("Proof General, " ^ msg ^ " " ^ quote (File.sysify_path path));
     1.7 +val tell_unlock = tell_file "you can unlock the file";
     1.8  
     1.9  end;
    1.10  
    1.11 @@ -204,7 +205,7 @@
    1.12    if action = ThyInfo.Update then
    1.13      seq (tell_file "this file is loaded:") (ThyInfo.loaded_files name)
    1.14    else if action = ThyInfo.Outdate orelse action = ThyInfo.Remove then
    1.15 -    seq (tell_file "you can unlock the file") (add_master_files name (ThyInfo.loaded_files name))
    1.16 +    seq tell_unlock (add_master_files name (ThyInfo.loaded_files name))
    1.17    else ();
    1.18  
    1.19  in
    1.20 @@ -215,7 +216,7 @@
    1.21  
    1.22  (* prepare theory context *)
    1.23  
    1.24 -val thy_name = Path.pack o Path.drop_ext o Path.base o Path.unpack;
    1.25 +val thy_name = Path.pack o #1 o Path.split_ext o Path.base o Path.unpack;
    1.26  val update_thy_only = setmp MetaSimplifier.trace_simp false ThyInfo.update_thy_only;
    1.27  
    1.28  fun which_context () =
    1.29 @@ -239,13 +240,18 @@
    1.30  
    1.31  fun proper_inform_file_processed file state =
    1.32    let val name = thy_name file in
    1.33 -    ThyInfo.if_known_thy ThyInfo.touch_child_thys name;
    1.34 -    if not (Toplevel.is_toplevel state) then
    1.35 -      warning ("Not at toplevel -- cannot register theory " ^ quote name)
    1.36 -    else transform_error ThyInfo.pretend_use_thy_only name handle ERROR_MESSAGE msg =>
    1.37 -      (warning msg; warning ("Failed to register theory " ^ quote name))
    1.38 +    if Toplevel.is_toplevel state andalso ThyInfo.known_thy name then
    1.39 +     (ThyInfo.touch_child_thys name;
    1.40 +      transform_error ThyInfo.pretend_use_thy_only name handle ERROR_MESSAGE msg =>
    1.41 +       (warning msg; warning ("Failed to register theory: " ^ quote name);
    1.42 +        tell_unlock (Path.base (Path.unpack file))))
    1.43 +    else raise Toplevel.UNDEF
    1.44    end;
    1.45  
    1.46 +fun vacuous_inform_file_processed file state =
    1.47 + (warning ("No theory " ^ quote (thy_name file));
    1.48 +  tell_unlock (Path.base (Path.unpack file)));
    1.49 +
    1.50  
    1.51  (* options *)
    1.52  
    1.53 @@ -423,13 +429,15 @@
    1.54  
    1.55  val inform_file_processedP =
    1.56    OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control
    1.57 -    (P.name >> (Toplevel.no_timing oo
    1.58 -      (fn name => Toplevel.keep (proper_inform_file_processed name))));
    1.59 +    (P.name >> (fn file => Toplevel.no_timing o
    1.60 +      Toplevel.keep (vacuous_inform_file_processed file) o
    1.61 +      Toplevel.kill o
    1.62 +      Toplevel.keep (proper_inform_file_processed file)));
    1.63  
    1.64  val inform_file_retractedP =
    1.65    OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control
    1.66      (P.name >> (Toplevel.no_timing oo
    1.67 -      (fn name => Toplevel.imperative (fn () => inform_file_retracted name))));
    1.68 +      (fn file => Toplevel.imperative (fn () => inform_file_retracted file))));
    1.69  
    1.70  val process_pgipP =
    1.71    OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" K.control