# HG changeset patch
# User wenzelm
# Date 1372086233 -7200
# Node ID c88354589b438dd3eec6255c3e4f94e9339f4578
# Parent  c54e551de6f914965d95618f5a2072b2e06522fd
more formal ProofGeneral command setup within theory Pure;
consider 'ProofGeneral.pr' as control command as well;

diff -r c54e551de6f9 -r c88354589b43 etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Mon Jun 24 13:54:57 2013 +0200
+++ b/etc/isar-keywords-ZF.el	Mon Jun 24 17:03:53 2013 +0200
@@ -255,6 +255,7 @@
     "ProofGeneral\\.inform_file_processed"
     "ProofGeneral\\.inform_file_retracted"
     "ProofGeneral\\.kill_proof"
+    "ProofGeneral\\.pr"
     "ProofGeneral\\.process_pgip"
     "ProofGeneral\\.restart"
     "ProofGeneral\\.undo"
@@ -279,7 +280,6 @@
 (defconst isar-keywords-diag
   '("ML_command"
     "ML_val"
-    "ProofGeneral\\.pr"
     "class_deps"
     "display_drafts"
     "find_consts"
diff -r c54e551de6f9 -r c88354589b43 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Mon Jun 24 13:54:57 2013 +0200
+++ b/etc/isar-keywords.el	Mon Jun 24 17:03:53 2013 +0200
@@ -361,6 +361,7 @@
     "ProofGeneral\\.inform_file_processed"
     "ProofGeneral\\.inform_file_retracted"
     "ProofGeneral\\.kill_proof"
+    "ProofGeneral\\.pr"
     "ProofGeneral\\.process_pgip"
     "ProofGeneral\\.restart"
     "ProofGeneral\\.undo"
@@ -385,7 +386,6 @@
 (defconst isar-keywords-diag
   '("ML_command"
     "ML_val"
-    "ProofGeneral\\.pr"
     "boogie_status"
     "class_deps"
     "code_deps"
diff -r c54e551de6f9 -r c88354589b43 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Mon Jun 24 13:54:57 2013 +0200
+++ b/src/Pure/Pure.thy	Mon Jun 24 17:03:53 2013 +0200
@@ -93,6 +93,9 @@
   and "end" :: thy_end % "theory"
   and "realizers" "realizability" "extract_type" "extract" :: thy_decl
   and "find_theorems" "find_consts" :: diag
+  and "ProofGeneral.process_pgip" "ProofGeneral.pr" "ProofGeneral.undo"
+    "ProofGeneral.restart" "ProofGeneral.kill_proof" "ProofGeneral.inform_file_processed"
+    "ProofGeneral.inform_file_retracted" :: control
 begin
 
 ML_file "Isar/isar_syn.ML"
diff -r c54e551de6f9 -r c88354589b43 src/Pure/Tools/proof_general.ML
--- a/src/Pure/Tools/proof_general.ML	Mon Jun 24 13:54:57 2013 +0200
+++ b/src/Pure/Tools/proof_general.ML	Mon Jun 24 17:03:53 2013 +0200
@@ -29,10 +29,16 @@
   val preference_string: category -> string option ->
     string Unsynchronized.ref -> string -> string -> unit
   val preference_option: category -> string option -> string -> string -> string -> unit
+  val process_pgip: string -> unit
+  val tell_clear_goals: unit -> unit
+  val tell_clear_response: unit -> unit
+  val inform_file_processed: string -> unit
+  val inform_file_retracted: string -> unit
   structure ThyLoad: sig val add_path: string -> unit end
   val thm_deps: bool Unsynchronized.ref
   val proof_generalN: string
   val init: unit -> unit
+  val restart: unit -> unit
 end;
 
 structure ProofGeneral: PROOF_GENERAL =
@@ -426,46 +432,5 @@
   Isar.init ();
   welcome ());
 
-
-
-(** Isar command syntax **)
-
-val _ =
-  Outer_Syntax.improper_command
-    (("ProofGeneral.process_pgip", Keyword.control), Position.none) "(internal)"
-    (Parse.text >> (fn str => Toplevel.imperative (fn () => process_pgip str)));
-
-val _ =
-  Outer_Syntax.improper_command
-    (("ProofGeneral.pr", Keyword.diag), Position.none) "print state (internal)"
-    (Scan.succeed (Toplevel.keep (fn state =>
-      if Toplevel.is_toplevel state orelse Toplevel.is_theory state then tell_clear_goals ()
-      else (Toplevel.quiet := false; Toplevel.print_state true state))));
-
-val _ = (*undo without output -- historical*)
-  Outer_Syntax.improper_command
-    (("ProofGeneral.undo", Keyword.control), Position.none) "(internal)"
-    (Scan.succeed (Toplevel.imperative (fn () => Isar.undo 1)));
-
-val _ =
-  Outer_Syntax.improper_command
-    (("ProofGeneral.restart", Keyword.control), Position.none) "(internal)"
-    (Parse.opt_unit >> (K (Toplevel.imperative restart)));
-
-val _ =
-  Outer_Syntax.improper_command
-    (("ProofGeneral.kill_proof", Keyword.control), Position.none) "(internal)"
-    (Scan.succeed (Toplevel.imperative (fn () => (Isar.kill_proof (); tell_clear_goals ()))));
-
-val _ =
-  Outer_Syntax.improper_command
-    (("ProofGeneral.inform_file_processed", Keyword.control), Position.none) "(internal)"
-    (Parse.name >> (fn file => Toplevel.imperative (fn () => inform_file_processed file)));
-
-val _ =
-  Outer_Syntax.improper_command
-    (("ProofGeneral.inform_file_retracted", Keyword.control), Position.none) "(internal)"
-    (Parse.name >> (fn file => Toplevel.imperative (fn () => inform_file_retracted file)));
-
 end;
 
diff -r c54e551de6f9 -r c88354589b43 src/Pure/Tools/proof_general_pure.ML
--- a/src/Pure/Tools/proof_general_pure.ML	Mon Jun 24 13:54:57 2013 +0200
+++ b/src/Pure/Tools/proof_general_pure.ML	Mon Jun 24 17:03:53 2013 +0200
@@ -2,9 +2,14 @@
     Author:     David Aspinall
     Author:     Makarius
 
-Proof General preferences for Isabelle/Pure.
+Proof General setup within theory Pure.
 *)
 
+structure ProofGeneral_Pure: sig end =
+struct
+
+(** preferences **)
+
 (* display *)
 
 val _ =
@@ -169,3 +174,50 @@
     "parallel-proofs"
     "Check proofs in parallel";
 
+
+
+(** command syntax **)
+
+val _ =
+  Outer_Syntax.improper_command
+    @{command_spec "ProofGeneral.process_pgip"} "(internal)"
+    (Parse.text >> (fn str => Toplevel.imperative (fn () => ProofGeneral.process_pgip str)));
+
+val _ =
+  Outer_Syntax.improper_command
+    @{command_spec "ProofGeneral.pr"} "(internal)"
+    (Scan.succeed (Toplevel.keep (fn state =>
+      if Toplevel.is_toplevel state orelse Toplevel.is_theory state
+      then ProofGeneral.tell_clear_goals ()
+      else (Toplevel.quiet := false; Toplevel.print_state true state))));
+
+val _ = (*undo without output -- historical*)
+  Outer_Syntax.improper_command
+    @{command_spec "ProofGeneral.undo"} "(internal)"
+    (Scan.succeed (Toplevel.imperative (fn () => Isar.undo 1)));
+
+val _ =
+  Outer_Syntax.improper_command
+    @{command_spec "ProofGeneral.restart"} "(internal)"
+    (Parse.opt_unit >> (K (Toplevel.imperative ProofGeneral.restart)));
+
+val _ =
+  Outer_Syntax.improper_command
+    @{command_spec "ProofGeneral.kill_proof"} "(internal)"
+    (Scan.succeed (Toplevel.imperative (fn () =>
+      (Isar.kill_proof (); ProofGeneral.tell_clear_goals ()))));
+
+val _ =
+  Outer_Syntax.improper_command
+    @{command_spec "ProofGeneral.inform_file_processed"} "(internal)"
+    (Parse.name >> (fn file => Toplevel.imperative (fn () =>
+      ProofGeneral.inform_file_processed file)));
+
+val _ =
+  Outer_Syntax.improper_command
+    @{command_spec "ProofGeneral.inform_file_retracted"} "(internal)"
+    (Parse.name >> (fn file => Toplevel.imperative (fn () =>
+      ProofGeneral.inform_file_retracted file)));
+
+end;
+