src/Pure/ProofGeneral/proof_general_pgip.ML
changeset 22028 c13f6b5bf2b8
parent 22014 4b70cbd96007
child 22042 64f8f5433f30
     1.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat Jan 06 20:56:44 2007 +0100
     1.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Sun Jan 07 14:05:44 2007 +0100
     1.3 @@ -224,26 +224,29 @@
     1.4  local
     1.5  
     1.6  fun statedisplay prts =
     1.7 -    let
     1.8 +    let 
     1.9          val display = Pretty.output (Pretty.chunks prts)
    1.10 +        (* TODO: add extra PGML markup for allow proof state navigation *)
    1.11          val statedisplay = XML.Elem("statedisplay",[], [XML.Rawtext display])
    1.12      in
    1.13          issue_pgip (Proofstate {pgml=[XML.Elem("pgml",[],[statedisplay])]})
    1.14      end
    1.15  
    1.16  fun print_current_goals n m st =
    1.17 -  statedisplay (Display.pretty_current_goals n m st)
    1.18 +  case (Display.pretty_current_goals n m st) of 
    1.19 +   [] => tell_clear_goals()
    1.20 + | prts => statedisplay prts
    1.21  
    1.22  fun print_state b st =
    1.23 -  statedisplay (Toplevel.pretty_state b st)
    1.24 +  case (Toplevel.pretty_state b st) of 
    1.25 +   [] => tell_clear_goals() 
    1.26 +  | prts => statedisplay prts
    1.27  
    1.28  in
    1.29  
    1.30  fun setup_state () =
    1.31    (Display.print_current_goals_fn := print_current_goals;
    1.32     Toplevel.print_state_fn := print_state);
    1.33 -      (*    Toplevel.prompt_state_fn := (fn s => suffix (special "372")
    1.34 -                                        (Toplevel.prompt_state_default s))); *)
    1.35  
    1.36  end;
    1.37  
    1.38 @@ -292,7 +295,6 @@
    1.39       tell_clear_goals ();
    1.40       tell_clear_response ();
    1.41       welcome ();
    1.42 -     priority "Running new version of PGIP code.  In testing.";
    1.43       raise Toplevel.RESTART)
    1.44  
    1.45  
    1.46 @@ -413,7 +415,7 @@
    1.47              "" => isarcmd ("use_thy " ^ quote (Path.implode path))
    1.48            | "thy" => isarcmd ("use_thy " ^ quote (Path.implode path))
    1.49            | "ML" => isarcmd ("use " ^ quote file)
    1.50 -          | other => error ("Don't know how to read a file with extension " ^ other)
    1.51 +          | other => error ("Don't know how to read a file with extension " ^ quote other)
    1.52      end
    1.53  
    1.54  
    1.55 @@ -727,9 +729,11 @@
    1.56        val openfile_retract = Output.no_warnings (ThyInfo.if_known_thy ThyInfo.remove_thy) o thy_name;
    1.57    in
    1.58        case !currently_open_file of
    1.59 -          SOME f => raise PGIP ("<openfile> when a file is already open! ")
    1.60 +          SOME f => raise PGIP ("<openfile> when a file is already open!\nCurrently open file: " ^
    1.61 +				PgipTypes.string_of_pgipurl url)
    1.62          | NONE => (openfile_retract filepath;
    1.63                     changecwd_dir filedir;
    1.64 +		   priority ("Working in file: " ^ PgipTypes.string_of_pgipurl url);
    1.65                     currently_open_file := SOME url)
    1.66    end
    1.67  
    1.68 @@ -737,6 +741,7 @@
    1.69      case !currently_open_file of
    1.70          SOME f => (proper_inform_file_processed (File.platform_path f)
    1.71                                                  (Isar.state());
    1.72 +		   priority ("Finished working in file: " ^ PgipTypes.string_of_pgipurl f);
    1.73                     currently_open_file := NONE)
    1.74        | NONE => raise PGIP ("<closefile> when no file is open!")
    1.75  
    1.76 @@ -745,13 +750,16 @@
    1.77          val url = #url vs
    1.78      in
    1.79          case !currently_open_file of
    1.80 -            SOME f => raise PGIP ("<loadfile> when a file is open!")
    1.81 +            SOME f => raise PGIP ("<loadfile> when a file is open!\nCurrently open file: " ^
    1.82 +				  PgipTypes.string_of_pgipurl url)
    1.83            | NONE => use_thy_or_ml_file (File.platform_path url)
    1.84      end
    1.85  
    1.86  fun abortfile vs =
    1.87      case !currently_open_file of
    1.88          SOME f => (isarcmd "init_toplevel";
    1.89 +		   priority ("Aborted working in file: " ^ 
    1.90 +			     PgipTypes.string_of_pgipurl f);
    1.91                     currently_open_file := NONE)
    1.92        | NONE => raise PGIP ("<abortfile> when no file is open!")
    1.93  
    1.94 @@ -761,7 +769,8 @@
    1.95      in
    1.96          case !currently_open_file of
    1.97              SOME f => raise PGIP ("<retractfile> when a file is open!")
    1.98 -          | NONE => inform_file_retracted (File.platform_path url)
    1.99 +          | NONE => (priority ("Retracting file: " ^ PgipTypes.string_of_pgipurl url);
   1.100 +		     inform_file_retracted (File.platform_path url))
   1.101      end
   1.102  
   1.103