# HG changeset patch
# User wenzelm
# Date 1392289791 -3600
# Node ID e42a3fc184582c699cfb0017f0957a6a0c968097
# Parent  aa41ecbdc20520d77b77c4ef564aaba09b6cfdad
explicit indication that redefining outer syntax commands is not supposed to happen -- NB: interactive mode requires global change of syntax;

diff -r aa41ecbdc205 -r e42a3fc18458 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Thu Feb 13 11:54:14 2014 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Thu Feb 13 12:09:51 2014 +0100
@@ -10,6 +10,7 @@
 signature OUTER_SYNTAX =
 sig
   type outer_syntax
+  val batch_mode: bool Unsynchronized.ref
   val is_markup: outer_syntax -> Thy_Output.markup -> string -> bool
   val get_syntax: unit -> (Scan.lexicon * Scan.lexicon) * outer_syntax
   val check_syntax: unit -> unit
@@ -133,6 +134,8 @@
 
 type command_spec = (string * Keyword.T) * Position.T;
 
+val batch_mode = Unsynchronized.ref false;
+
 local
 
 (*synchronized wrt. Keywords*)
@@ -153,10 +156,20 @@
           then Keyword.define (name, SOME kind)
           else error ("Undeclared outer syntax command " ^ quote name ^ Position.here pos));
     val _ = Position.report pos (command_markup true (name, cmd));
+
+    fun redefining () =
+      "Redefining outer syntax command " ^ quote name ^ Position.here (Position.thread_data ());
   in
     Unsynchronized.change global_outer_syntax (map_commands (fn commands =>
      (if not (Symtab.defined commands name) then ()
-      else warning ("Redefining outer syntax command " ^ quote name);
+      else
+        let
+          val _ = warning (redefining ());
+          val _ =
+            if ! batch_mode then
+              Output.physical_stderr ("Legacy feature! " ^ redefining () ^ "\n")
+            else ();
+        in () end;
       Symtab.update (name, cmd) commands)))
   end);
 
diff -r aa41ecbdc205 -r e42a3fc18458 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Thu Feb 13 11:54:14 2014 +0100
+++ b/src/Pure/Tools/build.ML	Thu Feb 13 12:09:51 2014 +0100
@@ -166,6 +166,7 @@
         theories |>
           (List.app (use_theories_condition last_timing)
             |> session_timing name verbose
+            |> Unsynchronized.setmp Outer_Syntax.batch_mode true
             |> Unsynchronized.setmp Output.protocol_message_fn protocol_message
             |> Multithreading.max_threads_setmp (Options.int options "threads")
             |> Exn.capture);