explicit indication that redefining outer syntax commands is not supposed to happen -- NB: interactive mode requires global change of syntax;
authorwenzelm
Thu Feb 13 12:09:51 2014 +0100 (2014-02-13 ago)
changeset 55448e42a3fc18458
parent 55447 aa41ecbdc205
child 55449 ce855dc0e523
explicit indication that redefining outer syntax commands is not supposed to happen -- NB: interactive mode requires global change of syntax;
src/Pure/Isar/outer_syntax.ML
src/Pure/Tools/build.ML
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Thu Feb 13 11:54:14 2014 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Thu Feb 13 12:09:51 2014 +0100
     1.3 @@ -10,6 +10,7 @@
     1.4  signature OUTER_SYNTAX =
     1.5  sig
     1.6    type outer_syntax
     1.7 +  val batch_mode: bool Unsynchronized.ref
     1.8    val is_markup: outer_syntax -> Thy_Output.markup -> string -> bool
     1.9    val get_syntax: unit -> (Scan.lexicon * Scan.lexicon) * outer_syntax
    1.10    val check_syntax: unit -> unit
    1.11 @@ -133,6 +134,8 @@
    1.12  
    1.13  type command_spec = (string * Keyword.T) * Position.T;
    1.14  
    1.15 +val batch_mode = Unsynchronized.ref false;
    1.16 +
    1.17  local
    1.18  
    1.19  (*synchronized wrt. Keywords*)
    1.20 @@ -153,10 +156,20 @@
    1.21            then Keyword.define (name, SOME kind)
    1.22            else error ("Undeclared outer syntax command " ^ quote name ^ Position.here pos));
    1.23      val _ = Position.report pos (command_markup true (name, cmd));
    1.24 +
    1.25 +    fun redefining () =
    1.26 +      "Redefining outer syntax command " ^ quote name ^ Position.here (Position.thread_data ());
    1.27    in
    1.28      Unsynchronized.change global_outer_syntax (map_commands (fn commands =>
    1.29       (if not (Symtab.defined commands name) then ()
    1.30 -      else warning ("Redefining outer syntax command " ^ quote name);
    1.31 +      else
    1.32 +        let
    1.33 +          val _ = warning (redefining ());
    1.34 +          val _ =
    1.35 +            if ! batch_mode then
    1.36 +              Output.physical_stderr ("Legacy feature! " ^ redefining () ^ "\n")
    1.37 +            else ();
    1.38 +        in () end;
    1.39        Symtab.update (name, cmd) commands)))
    1.40    end);
    1.41  
     2.1 --- a/src/Pure/Tools/build.ML	Thu Feb 13 11:54:14 2014 +0100
     2.2 +++ b/src/Pure/Tools/build.ML	Thu Feb 13 12:09:51 2014 +0100
     2.3 @@ -166,6 +166,7 @@
     2.4          theories |>
     2.5            (List.app (use_theories_condition last_timing)
     2.6              |> session_timing name verbose
     2.7 +            |> Unsynchronized.setmp Outer_Syntax.batch_mode true
     2.8              |> Unsynchronized.setmp Output.protocol_message_fn protocol_message
     2.9              |> Multithreading.max_threads_setmp (Options.int options "threads")
    2.10              |> Exn.capture);