discontinued separate Pure-ProofGeneral keywords session -- protocol commands are already defined in Pure;
authorwenzelm
Fri Aug 27 22:09:51 2010 +0200 (2010-08-27)
changeset 38837b47ee8df7ab4
parent 38836 52cee2c5f219
child 38838 62f6ba39b3d4
discontinued separate Pure-ProofGeneral keywords session -- protocol commands are already defined in Pure;
Admin/update-keywords
etc/isar-keywords-ZF.el
etc/isar-keywords.el
src/Pure/IsaMakefile
src/Pure/ProofGeneral/proof_general_emacs.ML
src/Pure/ProofGeneral/proof_general_keywords.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
     1.1 --- a/Admin/update-keywords	Fri Aug 27 21:23:31 2010 +0200
     1.2 +++ b/Admin/update-keywords	Fri Aug 27 22:09:51 2010 +0200
     1.3 @@ -11,9 +11,9 @@
     1.4  cd "$ISABELLE_HOME/etc"
     1.5  
     1.6  isabelle keywords \
     1.7 -  "$LOG/Pure.gz" "$LOG/Pure-ProofGeneral.gz" "$LOG/HOL.gz" "$LOG/HOLCF.gz" \
     1.8 -  "$LOG/HOL-Boogie.gz" "$LOG/HOL-Nominal.gz" "$LOG/HOL-Statespace.gz"
     1.9 +  "$LOG/Pure.gz" "$LOG/HOL.gz" "$LOG/HOLCF.gz" "$LOG/HOL-Boogie.gz" \
    1.10 +  "$LOG/HOL-Nominal.gz" "$LOG/HOL-Statespace.gz"
    1.11  
    1.12  isabelle keywords -k ZF \
    1.13 -  "$LOG/Pure.gz" "$LOG/Pure-ProofGeneral.gz" "$LOG/FOL.gz" "$LOG/ZF.gz"
    1.14 +  "$LOG/Pure.gz" "$LOG/FOL.gz" "$LOG/ZF.gz"
    1.15  
     2.1 --- a/etc/isar-keywords-ZF.el	Fri Aug 27 21:23:31 2010 +0200
     2.2 +++ b/etc/isar-keywords-ZF.el	Fri Aug 27 22:09:51 2010 +0200
     2.3 @@ -1,6 +1,6 @@
     2.4  ;;
     2.5  ;; Keyword classification tables for Isabelle/Isar.
     2.6 -;; Generated from Pure + Pure-ProofGeneral + FOL + ZF.
     2.7 +;; Generated from Pure + FOL + ZF.
     2.8  ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
     2.9  ;;
    2.10  
     3.1 --- a/etc/isar-keywords.el	Fri Aug 27 21:23:31 2010 +0200
     3.2 +++ b/etc/isar-keywords.el	Fri Aug 27 22:09:51 2010 +0200
     3.3 @@ -1,6 +1,6 @@
     3.4  ;;
     3.5  ;; Keyword classification tables for Isabelle/Isar.
     3.6 -;; Generated from Pure + Pure-ProofGeneral + HOL + HOLCF + HOL-Boogie + HOL-Nominal + HOL-Statespace.
     3.7 +;; Generated from Pure + HOL + HOLCF + HOL-Boogie + HOL-Nominal + HOL-Statespace.
     3.8  ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
     3.9  ;;
    3.10  
     4.1 --- a/src/Pure/IsaMakefile	Fri Aug 27 21:23:31 2010 +0200
     4.2 +++ b/src/Pure/IsaMakefile	Fri Aug 27 22:09:51 2010 +0200
     4.3 @@ -6,7 +6,7 @@
     4.4  
     4.5  default: Pure
     4.6  images: Pure
     4.7 -test: RAW Pure-ProofGeneral
     4.8 +test: RAW
     4.9  all: images test
    4.10  
    4.11  
    4.12 @@ -256,15 +256,7 @@
    4.13  	@./mk
    4.14  
    4.15  
    4.16 -## Proof General keywords
    4.17 -
    4.18 -Pure-ProofGeneral: Pure $(LOG)/Pure-ProofGeneral.gz
    4.19 -
    4.20 -$(LOG)/Pure-ProofGeneral.gz: $(OUT)/Pure ProofGeneral/proof_general_keywords.ML
    4.21 -	@$(ISABELLE_TOOL) usedir -f proof_general_keywords.ML $(OUT)/Pure ProofGeneral
    4.22 -
    4.23 -
    4.24  ## clean
    4.25  
    4.26  clean:
    4.27 -	@rm -f $(OUT)/Pure $(LOG)/Pure.gz $(OUT)/RAW $(LOG)/RAW.gz $(LOG)/Pure-ProofGeneral.gz
    4.28 +	@rm -f $(OUT)/Pure $(LOG)/Pure.gz $(OUT)/RAW $(LOG)/RAW.gz
     5.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Fri Aug 27 21:23:31 2010 +0200
     5.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Fri Aug 27 22:09:51 2010 +0200
     5.3 @@ -10,7 +10,6 @@
     5.4    val test_markupN: string
     5.5    val sendback: string -> Pretty.T list -> unit
     5.6    val init: bool -> unit
     5.7 -  val init_outer_syntax: unit -> unit
     5.8    structure ThyLoad: sig val add_path: string -> unit end
     5.9  end;
    5.10  
    5.11 @@ -20,7 +19,6 @@
    5.12  
    5.13  (* print modes *)
    5.14  
    5.15 -val proof_generalN = "ProofGeneralEmacs";  (*token markup (colouring vars, etc.)*)
    5.16  val thm_depsN = "thm_deps";                (*meta-information about theorem deps*)
    5.17  val test_markupN = "test_markup";          (*XML markup for everything*)
    5.18  
    5.19 @@ -187,44 +185,35 @@
    5.20  
    5.21  (* additional outer syntax for Isar *)
    5.22  
    5.23 -fun prP () =
    5.24 +val _ =
    5.25    Outer_Syntax.improper_command "ProofGeneral.pr" "print state (internal)" Keyword.diag
    5.26      (Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state =>
    5.27        if Toplevel.is_toplevel state orelse Toplevel.is_theory state then tell_clear_goals ()
    5.28        else (Toplevel.quiet := false; Toplevel.print_state true state))));
    5.29  
    5.30 -fun undoP () = (*undo without output -- historical*)
    5.31 +val _ = (*undo without output -- historical*)
    5.32    Outer_Syntax.improper_command "ProofGeneral.undo" "(internal)" Keyword.control
    5.33      (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Isar.undo 1)));
    5.34  
    5.35 -fun restartP () =
    5.36 +val _ =
    5.37    Outer_Syntax.improper_command "ProofGeneral.restart" "(internal)" Keyword.control
    5.38      (Parse.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative restart)));
    5.39  
    5.40 -fun kill_proofP () =
    5.41 +val _ =
    5.42    Outer_Syntax.improper_command "ProofGeneral.kill_proof" "(internal)" Keyword.control
    5.43      (Scan.succeed (Toplevel.no_timing o
    5.44        Toplevel.imperative (fn () => (Isar.kill_proof (); tell_clear_goals ()))));
    5.45  
    5.46 -fun inform_file_processedP () =
    5.47 +val _ =
    5.48    Outer_Syntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" Keyword.control
    5.49      (Parse.name >> (fn file =>
    5.50        Toplevel.no_timing o Toplevel.imperative (fn () => inform_file_processed file)));
    5.51  
    5.52 -fun inform_file_retractedP () =
    5.53 +val _ =
    5.54    Outer_Syntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" Keyword.control
    5.55      (Parse.name >> (Toplevel.no_timing oo
    5.56        (fn file => Toplevel.imperative (fn () => inform_file_retracted file))));
    5.57  
    5.58 -fun process_pgipP () =
    5.59 -  Outer_Syntax.improper_command "ProofGeneral.process_pgip" "(internal)" Keyword.control
    5.60 -    (Parse.text >> (Toplevel.no_timing oo
    5.61 -      (fn txt => Toplevel.imperative (fn () => ProofGeneralPgip.process_pgip txt))));
    5.62 -
    5.63 -fun init_outer_syntax () = List.app (fn f => f ())
    5.64 -  [prP, undoP, restartP, kill_proofP, inform_file_processedP,
    5.65 -    inform_file_retractedP, process_pgipP];
    5.66 -
    5.67  
    5.68  (* init *)
    5.69  
    5.70 @@ -234,17 +223,17 @@
    5.71    | init true =
    5.72        (if ! initialized then ()
    5.73         else
    5.74 -        (init_outer_syntax ();
    5.75 -         Output.add_mode Symbol.xsymbolsN Symbol.output Output.default_escape;
    5.76 -         Output.add_mode proof_generalN Output.default_output Output.default_escape;
    5.77 -         Markup.add_mode proof_generalN YXML.output_markup;
    5.78 +        (Output.add_mode Symbol.xsymbolsN Symbol.output Output.default_escape;
    5.79 +         Output.add_mode ProofGeneralPgip.proof_general_emacsN
    5.80 +          Output.default_output Output.default_escape;
    5.81 +         Markup.add_mode ProofGeneralPgip.proof_general_emacsN YXML.output_markup;
    5.82           setup_messages ();
    5.83 -         ProofGeneralPgip.init_pgip_channel (! Output.priority_fn);
    5.84 +         ProofGeneralPgip.pgip_channel_emacs (! Output.priority_fn);
    5.85           setup_thy_loader ();
    5.86           setup_present_hook ();
    5.87           initialized := true);
    5.88         sync_thy_loader ();
    5.89 -       Unsynchronized.change print_mode (update (op =) proof_generalN);
    5.90 +       Unsynchronized.change print_mode (update (op =) ProofGeneralPgip.proof_general_emacsN);
    5.91         Secure.PG_setup ();
    5.92         Isar.toplevel_loop TextIO.stdIn
    5.93          {init = true, welcome = true, sync = true, secure = Secure.is_secure ()});
     6.1 --- a/src/Pure/ProofGeneral/proof_general_keywords.ML	Fri Aug 27 21:23:31 2010 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,8 +0,0 @@
     6.4 -(*  Title:      Pure/ProofGeneral/proof_general_keywords.ML
     6.5 -    Author:     Makarius
     6.6 -
     6.7 -Dummy session with outer syntax keyword initialization.
     6.8 -*)
     6.9 -
    6.10 -ProofGeneral.init_outer_syntax ();
    6.11 -
     7.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Fri Aug 27 21:23:31 2010 +0200
     7.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Fri Aug 27 22:09:51 2010 +0200
     7.3 @@ -7,12 +7,12 @@
     7.4  
     7.5  signature PROOF_GENERAL_PGIP =
     7.6  sig
     7.7 +  val proof_general_emacsN: string
     7.8 +
     7.9    val new_thms_deps: theory -> theory -> string list * string list
    7.10    val init_pgip: bool -> unit             (* main PGIP loop with true; fail with false *)
    7.11  
    7.12 -  (* These two are just to support the semi-PGIP Emacs mode *)
    7.13 -  val init_pgip_channel: (string -> unit) -> unit
    7.14 -  val process_pgip: string -> unit
    7.15 +  val pgip_channel_emacs: (string -> unit) -> unit
    7.16  
    7.17    (* More message functions... *)
    7.18    val nonfatal_error : string -> unit     (* recoverable (batch) error: carry on scripting *)
    7.19 @@ -31,6 +31,7 @@
    7.20  
    7.21  (** print mode **)
    7.22  
    7.23 +val proof_general_emacsN = "ProofGeneralEmacs";
    7.24  val proof_generalN = "ProofGeneral";
    7.25  val pgmlsymbols_flag = Unsynchronized.ref true;
    7.26  
    7.27 @@ -315,8 +316,6 @@
    7.28          fun keyword_elt kind keyword =
    7.29              XML.Elem (("keyword", [("word", keyword), ("category", kind)]), [])
    7.30          in
    7.31 -            (* Also, note we don't call init_outer_syntax here to add interface commands,
    7.32 -            but they should never appear in scripts anyway so it shouldn't matter *)
    7.33              Lexicalstructure
    7.34                {content = map (keyword_elt "minor") keywords @ map (keyword_elt "major") commands}
    7.35          end
    7.36 @@ -1007,14 +1006,6 @@
    7.37  end
    7.38  
    7.39  
    7.40 -(* Extra command for embedding prover-control inside document (obscure/debug usage). *)
    7.41 -
    7.42 -fun init_outer_syntax () =
    7.43 -  Outer_Syntax.improper_command "ProofGeneral.process_pgip" "(internal)" Keyword.control
    7.44 -    (Parse.text >> (Toplevel.no_timing oo
    7.45 -      (fn txt => Toplevel.imperative (fn () => process_pgip_plain txt))));
    7.46 -
    7.47 -
    7.48  (* init *)
    7.49  
    7.50  val initialized = Unsynchronized.ref false;
    7.51 @@ -1027,7 +1018,6 @@
    7.52           Output.add_mode proof_generalN Output.default_output Output.default_escape;
    7.53           Markup.add_mode proof_generalN YXML.output_markup;
    7.54           setup_messages ();
    7.55 -         init_outer_syntax ();
    7.56           setup_thy_loader ();
    7.57           setup_present_hook ();
    7.58           init_pgip_session_id ();
    7.59 @@ -1046,16 +1036,27 @@
    7.60  in
    7.61  
    7.62  (* Set recipient for PGIP results *)
    7.63 -fun init_pgip_channel writefn =
    7.64 +fun pgip_channel_emacs writefn =
    7.65      (init_pgip_session_id();
    7.66       pgip_output_channel := writefn)
    7.67  
    7.68  (* Process a PGIP command.
    7.69     This works for preferences but not generally guaranteed
    7.70     because we haven't done full setup here (e.g., no pgml mode)  *)
    7.71 -fun process_pgip str =
    7.72 +fun process_pgip_emacs str =
    7.73       setmp_CRITICAL output_xml_fn (!pgip_output_channel) process_pgip_plain str
    7.74  
    7.75  end
    7.76  
    7.77 +
    7.78 +(* Extra command for embedding prover-control inside document (obscure/debug usage). *)
    7.79 +
    7.80 +val _ =
    7.81 +  Outer_Syntax.improper_command "ProofGeneral.process_pgip" "(internal)" Keyword.control
    7.82 +    (Parse.text >> (Toplevel.no_timing oo
    7.83 +      (fn txt => Toplevel.imperative (fn () =>
    7.84 +        if print_mode_active proof_general_emacsN
    7.85 +        then process_pgip_emacs txt
    7.86 +        else process_pgip_plain txt))));
    7.87 +
    7.88  end;