--- a/Admin/lib/Tools/update_keywords Wed Sep 04 13:45:46 2013 +0200
+++ b/Admin/lib/Tools/update_keywords Wed Sep 04 15:27:24 2013 +0200
@@ -3,6 +3,7 @@
# Author: Makarius
#
# DESCRIPTION: update standard keyword files for Emacs Proof General
+# (Proof General legacy)
isabelle_admin_build jars || exit $?
--- a/src/HOL/Tools/Sledgehammer/async_manager.ML Wed Sep 04 13:45:46 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/async_manager.ML Wed Sep 04 15:27:24 2013 +0200
@@ -6,6 +6,8 @@
Central manager for asynchronous diagnosis tool threads.
*)
+(*Proof General legacy*)
+
signature ASYNC_MANAGER =
sig
val break_into_chunks : string -> string list
--- a/src/Pure/General/output.ML Wed Sep 04 13:45:46 2013 +0200
+++ b/src/Pure/General/output.ML Wed Sep 04 15:27:24 2013 +0200
@@ -95,7 +95,7 @@
structure Internal =
struct
val writeln_fn = Unsynchronized.ref physical_writeln;
- val urgent_message_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
+ val urgent_message_fn = Unsynchronized.ref (fn s => ! writeln_fn s); (*Proof General legacy*)
val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
val warning_fn = Unsynchronized.ref (physical_writeln o prefix_lines "### ");
val error_fn = Unsynchronized.ref (fn (_: serial, s) => physical_writeln (prefix_lines "*** " s));
@@ -108,7 +108,7 @@
end;
fun writeln s = ! Internal.writeln_fn (output s);
-fun urgent_message s = ! Internal.urgent_message_fn (output s);
+fun urgent_message s = ! Internal.urgent_message_fn (output s); (*Proof General legacy*)
fun tracing s = ! Internal.tracing_fn (output s);
fun warning s = ! Internal.warning_fn (output s);
fun error_msg' (i, s) = ! Internal.error_fn (i, output s);
--- a/src/Pure/General/symbol.ML Wed Sep 04 13:45:46 2013 +0200
+++ b/src/Pure/General/symbol.ML Wed Sep 04 15:27:24 2013 +0200
@@ -113,6 +113,7 @@
fun not_eof s = s <> eof;
val stopper = Scan.stopper (K eof) is_eof;
+(*Proof General legacy*)
val sync = "\\<^sync>";
fun is_sync s = s = sync;
@@ -424,7 +425,7 @@
val scan_encoded_newline =
$$ "\^M" -- $$ "\n" >> K "\n" ||
$$ "\^M" >> K "\n" ||
- Scan.this_string "\\<^newline>" >> K "\n";
+ Scan.this_string "\\<^newline>" >> K "\n"; (*Proof General legacy*)
val scan_raw =
Scan.this_string "raw:" ^^ (Scan.many raw_chr >> implode) ||
--- a/src/Pure/Isar/isar_syn.ML Wed Sep 04 13:45:46 2013 +0200
+++ b/src/Pure/Isar/isar_syn.ML Wed Sep 04 15:27:24 2013 +0200
@@ -743,6 +743,7 @@
val opt_bang = Scan.optional (@{keyword "!"} >> K true) false;
+(*Proof General legacy*)
val _ =
Outer_Syntax.improper_command @{command_spec "pretty_setmargin"}
"change default margin for pretty printing"
@@ -958,7 +959,7 @@
"kill theory -- try to remove from loader database"
(Parse.name >> (fn name => Toplevel.imperative (fn () => Thy_Info.kill_thy name)));
-val _ =
+val _ = (*partial Proof General legacy*)
Outer_Syntax.improper_command @{command_spec "display_drafts"}
"display raw source files with symbols"
(Scan.repeat1 Parse.path >> (fn names =>
@@ -971,7 +972,7 @@
Toplevel.keep (fn state =>
Print_Mode.with_modes modes (Toplevel.print_state true) state)));
-val _ = (*historical, e.g. for ProofGeneral-3.7.x*)
+val _ = (*Proof General legacy, e.g. for ProofGeneral-3.7.x*)
Outer_Syntax.improper_command @{command_spec "pr"} "print current proof state (if present)"
(opt_modes -- Scan.option Parse.nat >> (fn (modes, limit) =>
Toplevel.keep (fn state =>
@@ -980,12 +981,12 @@
Toplevel.quiet := false;
Print_Mode.with_modes modes (Toplevel.print_state true) state))));
-val _ =
+val _ = (*Proof General legacy*)
Outer_Syntax.improper_command @{command_spec "disable_pr"}
"disable printing of toplevel state"
(Scan.succeed (Toplevel.imperative (fn () => Toplevel.quiet := true)));
-val _ =
+val _ = (*Proof General legacy*)
Outer_Syntax.improper_command @{command_spec "enable_pr"}
"enable printing of toplevel state"
(Scan.succeed (Toplevel.imperative (fn () => Toplevel.quiet := false)));
--- a/src/Pure/Isar/toplevel.ML Wed Sep 04 13:45:46 2013 +0200
+++ b/src/Pure/Isar/toplevel.ML Wed Sep 04 15:27:24 2013 +0200
@@ -225,10 +225,10 @@
(** toplevel transitions **)
-val quiet = Unsynchronized.ref false;
+val quiet = Unsynchronized.ref false; (*Proof General legacy*)
val debug = Runtime.debug;
-val interact = Unsynchronized.ref false;
-val timing = Unsynchronized.ref false;
+val interact = Unsynchronized.ref false; (*Proof General legacy*)
+val timing = Unsynchronized.ref false; (*Proof General legacy*)
val profiling = Unsynchronized.ref 0;
fun program body =
@@ -327,7 +327,7 @@
datatype transition = Transition of
{name: string, (*command name*)
pos: Position.T, (*source position*)
- int_only: bool, (*interactive-only*)
+ int_only: bool, (*interactive-only*) (* TTY / Proof General legacy*)
print: bool, (*print result state*)
timing: Time.time option, (*prescient timing information*)
trans: trans list}; (*primitive transitions (union)*)
@@ -556,10 +556,12 @@
(fn Proof (prf, x) => Proof (f prf, x)
| _ => raise UNDEF));
+(*Proof General legacy*)
fun skip_proof f = transaction (fn _ =>
(fn Skipped_Proof (h, x) => Skipped_Proof (f h, x)
| _ => raise UNDEF));
+(*Proof General legacy*)
fun skip_proof_to_theory pred = transaction (fn _ =>
(fn Skipped_Proof (d, (gthy, _)) => if pred d then Theory (gthy, NONE) else raise UNDEF
| _ => raise UNDEF));
--- a/src/Pure/Thy/thy_load.ML Wed Sep 04 13:45:46 2013 +0200
+++ b/src/Pure/Thy/thy_load.ML Wed Sep 04 15:27:24 2013 +0200
@@ -292,7 +292,7 @@
end));
-(* global master path *)
+(* global master path *) (*Proof General legacy*)
local
val master_path = Unsynchronized.ref Path.current;
--- a/src/Pure/Tools/proof_general.ML Wed Sep 04 13:45:46 2013 +0200
+++ b/src/Pure/Tools/proof_general.ML Wed Sep 04 15:27:24 2013 +0200
@@ -6,6 +6,8 @@
See also http://proofgeneral.inf.ed.ac.uk
*)
+(*Proof General legacy*)
+
signature PROOF_GENERAL =
sig
type category = string
--- a/src/Pure/Tools/proof_general_pure.ML Wed Sep 04 13:45:46 2013 +0200
+++ b/src/Pure/Tools/proof_general_pure.ML Wed Sep 04 15:27:24 2013 +0200
@@ -5,6 +5,8 @@
Proof General setup within theory Pure.
*)
+(*Proof General legacy*)
+
structure ProofGeneral_Pure: sig end =
struct