Initialise parser at startup. Remove some obsolete ProofGeneral.XXX outer syntax, mapping PGIP commands directly to Isar.
authoraspinall
Sun Dec 31 14:55:35 2006 +0100 (2006-12-31)
changeset 219721b68312c4cf0
parent 21971 513e1d82640d
child 21973 e7c9b0d3ce82
Initialise parser at startup. Remove some obsolete ProofGeneral.XXX outer syntax, mapping PGIP commands directly to Isar.
src/Pure/ProofGeneral/proof_general_pgip.ML
     1.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Sun Dec 31 14:50:40 2006 +0100
     1.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Sun Dec 31 14:55:35 2006 +0100
     1.3 @@ -281,10 +281,6 @@
     1.4      else raise Toplevel.UNDEF
     1.5    end;
     1.6  
     1.7 -fun vacuous_inform_file_processed file state =
     1.8 - (warning ("No theory " ^ quote (thy_name file));
     1.9 -  tell_file_retracted (Path.base (Path.explode file)));
    1.10 -
    1.11  
    1.12  (* restart top-level loop (keeps most state information) *)
    1.13  
    1.14 @@ -506,7 +502,7 @@
    1.15  
    1.16  fun redostep vs = isarcmd "redo"
    1.17  
    1.18 -fun abortgoal vs = isarcmd "ProofGeneral.kill_proof"
    1.19 +fun abortgoal vs = isarcmd "kill" (* was: ProofGeneral.kill_proof *)
    1.20  
    1.21  
    1.22  (*** PGIP identifier tables ***)
    1.23 @@ -673,13 +669,13 @@
    1.24      end
    1.25  
    1.26  fun undoitem vs =
    1.27 -    isarcmd "ProofGeneral.undo"
    1.28 +    isarcmd "undo"
    1.29  
    1.30  fun redoitem vs =
    1.31 -    isarcmd "ProofGeneral.redo"
    1.32 +    isarcmd "redo"
    1.33  
    1.34  fun aborttheory vs =
    1.35 -    isarcmd "init_toplevel"
    1.36 +    isarcmd "kill"  (* was: "init_toplevel" *)
    1.37  
    1.38  fun retracttheory (Retracttheory vs) =
    1.39      let
    1.40 @@ -922,49 +918,20 @@
    1.41  end
    1.42  
    1.43  
    1.44 -(* additional outer syntax for Isar *)
    1.45 -(* da: TODO: perhaps we can drop this superfluous syntax now??
    1.46 -   Seems cleaner to support the operations directly above in the PGIP actions.
    1.47 - *)
    1.48 -
    1.49 -local structure P = OuterParse and K = OuterKeyword in
    1.50 -
    1.51 -val undoP = (*undo without output*)
    1.52 -  OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
    1.53 -    (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
    1.54 -
    1.55 -val redoP = (*redo without output*)
    1.56 -  OuterSyntax.improper_command "ProofGeneral.redo" "(internal)" K.control
    1.57 -    (Scan.succeed (Toplevel.no_timing o IsarCmd.redo));
    1.58 +local
    1.59 +(* Extra command for embedding prover-control inside document (obscure/debug usage). *)
    1.60  
    1.61 -(* ProofGeneral.kill_proof still used above *)
    1.62 -val kill_proofP =
    1.63 -  OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control
    1.64 -    (Scan.succeed (Toplevel.no_timing o IsarCmd.kill_proof_notify tell_clear_goals));
    1.65 -
    1.66 -(* FIXME: Not quite same as commands used above *)
    1.67 -val inform_file_processedP =
    1.68 -  OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control
    1.69 -    (P.name >> (fn file => Toplevel.no_timing o
    1.70 -      Toplevel.init_empty (vacuous_inform_file_processed file) o
    1.71 -      Toplevel.kill o
    1.72 -      Toplevel.init_empty (proper_inform_file_processed file)));
    1.73 -
    1.74 -val inform_file_retractedP =
    1.75 -  OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control
    1.76 -    (P.name >> (Toplevel.no_timing oo
    1.77 -      (fn file => Toplevel.imperative (fn () => inform_file_retracted file))));
    1.78 -
    1.79 -(* This one can actually be used for Daniel's interface scripting idea: generically!! *)
    1.80 -val process_pgipP =
    1.81 -  OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" K.control
    1.82 -    (P.text >> (Toplevel.no_timing oo
    1.83 +val process_pgipP = 
    1.84 +  OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" OuterKeyword.control
    1.85 +    (OuterParse.text >> (Toplevel.no_timing oo
    1.86        (fn txt => Toplevel.imperative (fn () => process_pgip_plain txt))));
    1.87  
    1.88 -fun init_outer_syntax () = OuterSyntax.add_parsers
    1.89 - [undoP, redoP, kill_proofP, inform_file_processedP, inform_file_retractedP, process_pgipP];
    1.90 +in
    1.91  
    1.92 -end;
    1.93 + fun init_outer_syntax () = OuterSyntax.add_parsers [process_pgipP];
    1.94 +
    1.95 +end
    1.96 +
    1.97  
    1.98  
    1.99  (* init *)
   1.100 @@ -976,6 +943,7 @@
   1.101    | init_pgip true =
   1.102        (! initialized orelse
   1.103          (setmp warning_fn (K ()) init_outer_syntax ();
   1.104 +	  PgipParser.init ();
   1.105            setup_xsymbols_output ();
   1.106            setup_pgml_output ();
   1.107            setup_messages ();