1.1 --- a/etc/isar-keywords-ZF.el	Mon Jun 24 13:54:57 2013 +0200
     1.2 +++ b/etc/isar-keywords-ZF.el	Mon Jun 24 17:03:53 2013 +0200
     1.3 @@ -255,6 +255,7 @@
     1.4      "ProofGeneral\\.inform_file_processed"
     1.5      "ProofGeneral\\.inform_file_retracted"
     1.6      "ProofGeneral\\.kill_proof"
     1.7 +    "ProofGeneral\\.pr"
     1.8      "ProofGeneral\\.process_pgip"
     1.9      "ProofGeneral\\.restart"
    1.10      "ProofGeneral\\.undo"
    1.11 @@ -279,7 +280,6 @@
    1.12  (defconst isar-keywords-diag
    1.13    '("ML_command"
    1.14      "ML_val"
    1.15 -    "ProofGeneral\\.pr"
    1.16      "class_deps"
    1.17      "display_drafts"
    1.18      "find_consts"

     2.1 --- a/etc/isar-keywords.el	Mon Jun 24 13:54:57 2013 +0200
     2.2 +++ b/etc/isar-keywords.el	Mon Jun 24 17:03:53 2013 +0200
     2.3 @@ -361,6 +361,7 @@
     2.4      "ProofGeneral\\.inform_file_processed"
     2.5      "ProofGeneral\\.inform_file_retracted"
     2.6      "ProofGeneral\\.kill_proof"
     2.7 +    "ProofGeneral\\.pr"
     2.8      "ProofGeneral\\.process_pgip"
     2.9      "ProofGeneral\\.restart"
    2.10      "ProofGeneral\\.undo"
    2.11 @@ -385,7 +386,6 @@
    2.12  (defconst isar-keywords-diag
    2.13    '("ML_command"
    2.14      "ML_val"
    2.15 -    "ProofGeneral\\.pr"
    2.16      "boogie_status"
    2.17      "class_deps"
    2.18      "code_deps"

     3.1 --- a/src/Pure/Pure.thy	Mon Jun 24 13:54:57 2013 +0200
     3.2 +++ b/src/Pure/Pure.thy	Mon Jun 24 17:03:53 2013 +0200
     3.3 @@ -93,6 +93,9 @@
     3.4    and "end" :: thy_end % "theory"
     3.5    and "realizers" "realizability" "extract_type" "extract" :: thy_decl
     3.6    and "find_theorems" "find_consts" :: diag
     3.7 +  and "ProofGeneral.process_pgip" "ProofGeneral.pr" "ProofGeneral.undo"
     3.8 +    "ProofGeneral.restart" "ProofGeneral.kill_proof" "ProofGeneral.inform_file_processed"
     3.9 +    "ProofGeneral.inform_file_retracted" :: control
    3.10  begin
    3.11  
    3.12  ML_file "Isar/isar_syn.ML"

     4.1 --- a/src/Pure/Tools/proof_general.ML	Mon Jun 24 13:54:57 2013 +0200
     4.2 +++ b/src/Pure/Tools/proof_general.ML	Mon Jun 24 17:03:53 2013 +0200
     4.3 @@ -29,10 +29,16 @@
     4.4    val preference_string: category -> string option ->
     4.5      string Unsynchronized.ref -> string -> string -> unit
     4.6    val preference_option: category -> string option -> string -> string -> string -> unit
     4.7 +  val process_pgip: string -> unit
     4.8 +  val tell_clear_goals: unit -> unit
     4.9 +  val tell_clear_response: unit -> unit
    4.10 +  val inform_file_processed: string -> unit
    4.11 +  val inform_file_retracted: string -> unit
    4.12    structure ThyLoad: sig val add_path: string -> unit end
    4.13    val thm_deps: bool Unsynchronized.ref
    4.14    val proof_generalN: string
    4.15    val init: unit -> unit
    4.16 +  val restart: unit -> unit
    4.17  end;
    4.18  
    4.19  structure ProofGeneral: PROOF_GENERAL =
    4.20 @@ -426,46 +432,5 @@
    4.21    Isar.init ();
    4.22    welcome ());
    4.23  
    4.24 -
    4.25 -
    4.26 -(** Isar command syntax **)
    4.27 -
    4.28 -val _ =
    4.29 -  Outer_Syntax.improper_command
    4.30 -    (("ProofGeneral.process_pgip", Keyword.control), Position.none) "(internal)"
    4.31 -    (Parse.text >> (fn str => Toplevel.imperative (fn () => process_pgip str)));
    4.32 -
    4.33 -val _ =
    4.34 -  Outer_Syntax.improper_command
    4.35 -    (("ProofGeneral.pr", Keyword.diag), Position.none) "print state (internal)"
    4.36 -    (Scan.succeed (Toplevel.keep (fn state =>
    4.37 -      if Toplevel.is_toplevel state orelse Toplevel.is_theory state then tell_clear_goals ()
    4.38 -      else (Toplevel.quiet := false; Toplevel.print_state true state))));
    4.39 -
    4.40 -val _ = (*undo without output -- historical*)
    4.41 -  Outer_Syntax.improper_command
    4.42 -    (("ProofGeneral.undo", Keyword.control), Position.none) "(internal)"
    4.43 -    (Scan.succeed (Toplevel.imperative (fn () => Isar.undo 1)));
    4.44 -
    4.45 -val _ =
    4.46 -  Outer_Syntax.improper_command
    4.47 -    (("ProofGeneral.restart", Keyword.control), Position.none) "(internal)"
    4.48 -    (Parse.opt_unit >> (K (Toplevel.imperative restart)));
    4.49 -
    4.50 -val _ =
    4.51 -  Outer_Syntax.improper_command
    4.52 -    (("ProofGeneral.kill_proof", Keyword.control), Position.none) "(internal)"
    4.53 -    (Scan.succeed (Toplevel.imperative (fn () => (Isar.kill_proof (); tell_clear_goals ()))));
    4.54 -
    4.55 -val _ =
    4.56 -  Outer_Syntax.improper_command
    4.57 -    (("ProofGeneral.inform_file_processed", Keyword.control), Position.none) "(internal)"
    4.58 -    (Parse.name >> (fn file => Toplevel.imperative (fn () => inform_file_processed file)));
    4.59 -
    4.60 -val _ =
    4.61 -  Outer_Syntax.improper_command
    4.62 -    (("ProofGeneral.inform_file_retracted", Keyword.control), Position.none) "(internal)"
    4.63 -    (Parse.name >> (fn file => Toplevel.imperative (fn () => inform_file_retracted file)));
    4.64 -
    4.65  end;
    4.66  

     5.1 --- a/src/Pure/Tools/proof_general_pure.ML	Mon Jun 24 13:54:57 2013 +0200
     5.2 +++ b/src/Pure/Tools/proof_general_pure.ML	Mon Jun 24 17:03:53 2013 +0200
     5.3 @@ -2,9 +2,14 @@
     5.4      Author:     David Aspinall
     5.5      Author:     Makarius
     5.6  
     5.7 -Proof General preferences for Isabelle/Pure.
     5.8 +Proof General setup within theory Pure.
     5.9  *)
    5.10  
    5.11 +structure ProofGeneral_Pure: sig end =
    5.12 +struct
    5.13 +
    5.14 +(** preferences **)
    5.15 +
    5.16  (* display *)
    5.17  
    5.18  val _ =
    5.19 @@ -169,3 +174,50 @@
    5.20      "parallel-proofs"
    5.21      "Check proofs in parallel";
    5.22  
    5.23 +
    5.24 +
    5.25 +(** command syntax **)
    5.26 +
    5.27 +val _ =
    5.28 +  Outer_Syntax.improper_command
    5.29 +    @{command_spec "ProofGeneral.process_pgip"} "(internal)"
    5.30 +    (Parse.text >> (fn str => Toplevel.imperative (fn () => ProofGeneral.process_pgip str)));
    5.31 +
    5.32 +val _ =
    5.33 +  Outer_Syntax.improper_command
    5.34 +    @{command_spec "ProofGeneral.pr"} "(internal)"
    5.35 +    (Scan.succeed (Toplevel.keep (fn state =>
    5.36 +      if Toplevel.is_toplevel state orelse Toplevel.is_theory state
    5.37 +      then ProofGeneral.tell_clear_goals ()
    5.38 +      else (Toplevel.quiet := false; Toplevel.print_state true state))));
    5.39 +
    5.40 +val _ = (*undo without output -- historical*)
    5.41 +  Outer_Syntax.improper_command
    5.42 +    @{command_spec "ProofGeneral.undo"} "(internal)"
    5.43 +    (Scan.succeed (Toplevel.imperative (fn () => Isar.undo 1)));
    5.44 +
    5.45 +val _ =
    5.46 +  Outer_Syntax.improper_command
    5.47 +    @{command_spec "ProofGeneral.restart"} "(internal)"
    5.48 +    (Parse.opt_unit >> (K (Toplevel.imperative ProofGeneral.restart)));
    5.49 +
    5.50 +val _ =
    5.51 +  Outer_Syntax.improper_command
    5.52 +    @{command_spec "ProofGeneral.kill_proof"} "(internal)"
    5.53 +    (Scan.succeed (Toplevel.imperative (fn () =>
    5.54 +      (Isar.kill_proof (); ProofGeneral.tell_clear_goals ()))));
    5.55 +
    5.56 +val _ =
    5.57 +  Outer_Syntax.improper_command
    5.58 +    @{command_spec "ProofGeneral.inform_file_processed"} "(internal)"
    5.59 +    (Parse.name >> (fn file => Toplevel.imperative (fn () =>
    5.60 +      ProofGeneral.inform_file_processed file)));
    5.61 +
    5.62 +val _ =
    5.63 +  Outer_Syntax.improper_command
    5.64 +    @{command_spec "ProofGeneral.inform_file_retracted"} "(internal)"
    5.65 +    (Parse.name >> (fn file => Toplevel.imperative (fn () =>
    5.66 +      ProofGeneral.inform_file_retracted file)));
    5.67 +
    5.68 +end;
    5.69 +