src/Pure/ProofGeneral/proof_general_pgip.ML

       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))))
     else raise Toplevel.UNDEF
   end;
-
-fun vacuous_inform_file_processed file state =
- (warning ("No theory " ^ quote (thy_name file));
-  tell_file_retracted (Path.base (Path.explode file)));
 
 
 (* restart top-level loop (keeps most state information) *)
 
 val welcome = priority o Session.welcome;

         isarcmd ("undos_proof " ^ Int.toString times)
     end
 
 fun redostep vs = isarcmd "redo"
 
-fun abortgoal vs = isarcmd "ProofGeneral.kill_proof"
+fun abortgoal vs = isarcmd "kill" (* was: ProofGeneral.kill_proof *)
 
 
 (*** PGIP identifier tables ***)
 
 fun setids t = issue_pgip (Setids {idtables = [t]})

     in
         isarcmd text
     end
 
 fun undoitem vs =
-    isarcmd "ProofGeneral.undo"
+    isarcmd "undo"
 
 fun redoitem vs =
-    isarcmd "ProofGeneral.redo"
+    isarcmd "redo"
 
 fun aborttheory vs =
-    isarcmd "init_toplevel"
+    isarcmd "kill"  (* was: "init_toplevel" *)
 
 fun retracttheory (Retracttheory vs) =
     let
         val thyname = #thyname vs
     in

 
   fun pgip_toplevel x = loop true x
 end
 
 
-(* additional outer syntax for Isar *)
-(* da: TODO: perhaps we can drop this superfluous syntax now??
-   Seems cleaner to support the operations directly above in the PGIP actions.
- *)
-
-local structure P = OuterParse and K = OuterKeyword in
-
-val undoP = (*undo without output*)
-  OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
-    (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
-
-val redoP = (*redo without output*)
-  OuterSyntax.improper_command "ProofGeneral.redo" "(internal)" K.control
-    (Scan.succeed (Toplevel.no_timing o IsarCmd.redo));
-
-(* ProofGeneral.kill_proof still used above *)
-val kill_proofP =
-  OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control
-    (Scan.succeed (Toplevel.no_timing o IsarCmd.kill_proof_notify tell_clear_goals));
-
-(* FIXME: Not quite same as commands used above *)
-val inform_file_processedP =
-  OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control
-    (P.name >> (fn file => Toplevel.no_timing o
-      Toplevel.init_empty (vacuous_inform_file_processed file) o
-      Toplevel.kill o
-      Toplevel.init_empty (proper_inform_file_processed file)));
-
-val inform_file_retractedP =
-  OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control
-    (P.name >> (Toplevel.no_timing oo
-      (fn file => Toplevel.imperative (fn () => inform_file_retracted file))));
-
-(* This one can actually be used for Daniel's interface scripting idea: generically!! *)
-val process_pgipP =
-  OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" K.control
-    (P.text >> (Toplevel.no_timing oo
+local
+(* Extra command for embedding prover-control inside document (obscure/debug usage). *)
+
+val process_pgipP = 
+  OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" OuterKeyword.control
+    (OuterParse.text >> (Toplevel.no_timing oo
       (fn txt => Toplevel.imperative (fn () => process_pgip_plain txt))));
 
-fun init_outer_syntax () = OuterSyntax.add_parsers
- [undoP, redoP, kill_proofP, inform_file_processedP, inform_file_retractedP, process_pgipP];
-
-end;
+in
+
+ fun init_outer_syntax () = OuterSyntax.add_parsers [process_pgipP];
+
+end
+
 
 
 (* init *)
 
 val initialized = ref false;

 fun init_pgip false =
       Output.panic "No Proof General interface support for Isabelle/classic mode."
   | init_pgip true =
       (! initialized orelse
         (setmp warning_fn (K ()) init_outer_syntax ();
+	  PgipParser.init ();
           setup_xsymbols_output ();
           setup_pgml_output ();
           setup_messages ();
           setup_state ();
           setup_thy_loader ();