src/Pure/Thy/thy_output.ML
changeset 32738 15bb09ca0378
parent 30683 e8ac1f9d9469
child 32890 77df12652210
     1.1 --- a/src/Pure/Thy/thy_output.ML	Tue Sep 29 11:48:32 2009 +0200
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Tue Sep 29 11:49:22 2009 +0200
     1.3 @@ -6,11 +6,11 @@
     1.4  
     1.5  signature THY_OUTPUT =
     1.6  sig
     1.7 -  val display: bool ref
     1.8 -  val quotes: bool ref
     1.9 -  val indent: int ref
    1.10 -  val source: bool ref
    1.11 -  val break: bool ref
    1.12 +  val display: bool Unsynchronized.ref
    1.13 +  val quotes: bool Unsynchronized.ref
    1.14 +  val indent: int Unsynchronized.ref
    1.15 +  val source: bool Unsynchronized.ref
    1.16 +  val break: bool Unsynchronized.ref
    1.17    val add_commands: (string * (Args.src -> Toplevel.state -> string)) list -> unit
    1.18    val add_options: (string * (string -> (unit -> string) -> unit -> string)) list -> unit
    1.19    val defined_command: string -> bool
    1.20 @@ -21,7 +21,7 @@
    1.21    val antiquotation: string -> 'a context_parser ->
    1.22      ({state: Toplevel.state, source: Args.src, context: Proof.context} -> 'a -> string) -> unit
    1.23    datatype markup = Markup | MarkupEnv | Verbatim
    1.24 -  val modes: string list ref
    1.25 +  val modes: string list Unsynchronized.ref
    1.26    val eval_antiquote: Scan.lexicon -> Toplevel.state -> Symbol_Pos.text * Position.T -> string
    1.27    val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
    1.28      (Toplevel.transition * Toplevel.state) list -> (OuterLex.token, 'a) Source.source -> Buffer.T
    1.29 @@ -42,11 +42,11 @@
    1.30  
    1.31  (** global options **)
    1.32  
    1.33 -val display = ref false;
    1.34 -val quotes = ref false;
    1.35 -val indent = ref 0;
    1.36 -val source = ref false;
    1.37 -val break = ref false;
    1.38 +val display = Unsynchronized.ref false;
    1.39 +val quotes = Unsynchronized.ref false;
    1.40 +val indent = Unsynchronized.ref 0;
    1.41 +val source = Unsynchronized.ref false;
    1.42 +val break = Unsynchronized.ref false;
    1.43  
    1.44  
    1.45  
    1.46 @@ -55,10 +55,10 @@
    1.47  local
    1.48  
    1.49  val global_commands =
    1.50 -  ref (Symtab.empty: (Args.src -> Toplevel.state -> string) Symtab.table);
    1.51 +  Unsynchronized.ref (Symtab.empty: (Args.src -> Toplevel.state -> string) Symtab.table);
    1.52  
    1.53  val global_options =
    1.54 -  ref (Symtab.empty: (string -> (unit -> string) -> unit -> string) Symtab.table);
    1.55 +  Unsynchronized.ref (Symtab.empty: (string -> (unit -> string) -> unit -> string) Symtab.table);
    1.56  
    1.57  fun add_item kind (name, x) tab =
    1.58   (if not (Symtab.defined tab name) then ()
    1.59 @@ -67,8 +67,10 @@
    1.60  
    1.61  in
    1.62  
    1.63 -fun add_commands xs = CRITICAL (fn () => change global_commands (fold (add_item "command") xs));
    1.64 -fun add_options xs = CRITICAL (fn () => change global_options (fold (add_item "option") xs));
    1.65 +fun add_commands xs =
    1.66 +  CRITICAL (fn () => Unsynchronized.change global_commands (fold (add_item "command") xs));
    1.67 +fun add_options xs =
    1.68 +  CRITICAL (fn () => Unsynchronized.change global_options (fold (add_item "option") xs));
    1.69  
    1.70  fun defined_command name = Symtab.defined (! global_commands) name;
    1.71  fun defined_option name = Symtab.defined (! global_options) name;
    1.72 @@ -143,7 +145,7 @@
    1.73  
    1.74  (* eval_antiquote *)
    1.75  
    1.76 -val modes = ref ([]: string list);
    1.77 +val modes = Unsynchronized.ref ([]: string list);
    1.78  
    1.79  fun eval_antiquote lex state (txt, pos) =
    1.80    let