# HG changeset patch
# User wenzelm
# Date 1378301244 -7200
# Node ID c09f4005d6bd446aafedf3dc4d1686e6e8b22abf
# Parent  50cc036f152264169108ee2a73f59fdc023c6a81
some explicit indication of Proof General legacy;

diff -r 50cc036f1522 -r c09f4005d6bd Admin/lib/Tools/update_keywords
--- 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 $?
 
diff -r 50cc036f1522 -r c09f4005d6bd src/HOL/Tools/Sledgehammer/async_manager.ML
--- 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
diff -r 50cc036f1522 -r c09f4005d6bd src/Pure/General/output.ML
--- 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);
diff -r 50cc036f1522 -r c09f4005d6bd src/Pure/General/symbol.ML
--- 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) ||
diff -r 50cc036f1522 -r c09f4005d6bd src/Pure/Isar/isar_syn.ML
--- 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)));
diff -r 50cc036f1522 -r c09f4005d6bd src/Pure/Isar/toplevel.ML
--- 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));
diff -r 50cc036f1522 -r c09f4005d6bd src/Pure/Thy/thy_load.ML
--- 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;
diff -r 50cc036f1522 -r c09f4005d6bd src/Pure/Tools/proof_general.ML
--- 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
diff -r 50cc036f1522 -r c09f4005d6bd src/Pure/Tools/proof_general_pure.ML
--- 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