src/Pure/Syntax/syntax.ML
changeset 32738 15bb09ca0378
parent 30573 49899f26fbd1
child 32784 1a5dde5079ac
     1.1 --- a/src/Pure/Syntax/syntax.ML	Tue Sep 29 11:48:32 2009 +0200
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Tue Sep 29 11:49:22 2009 +0200
     1.3 @@ -36,9 +36,9 @@
     1.4    val print_syntax: syntax -> unit
     1.5    val guess_infix: syntax -> string -> mixfix option
     1.6    val read_token: string -> Symbol_Pos.T list * Position.T
     1.7 -  val ambiguity_is_error: bool ref
     1.8 -  val ambiguity_level: int ref
     1.9 -  val ambiguity_limit: int ref
    1.10 +  val ambiguity_is_error: bool Unsynchronized.ref
    1.11 +  val ambiguity_level: int Unsynchronized.ref
    1.12 +  val ambiguity_limit: int Unsynchronized.ref
    1.13    val standard_parse_term: Pretty.pp -> (term -> string option) ->
    1.14      (((string * int) * sort) list -> string * int -> Term.sort) ->
    1.15      (string -> bool * string) -> (string -> string option) ->
    1.16 @@ -472,9 +472,9 @@
    1.17  
    1.18  (* read_ast *)
    1.19  
    1.20 -val ambiguity_is_error = ref false;
    1.21 -val ambiguity_level = ref 1;
    1.22 -val ambiguity_limit = ref 10;
    1.23 +val ambiguity_is_error = Unsynchronized.ref false;
    1.24 +val ambiguity_level = Unsynchronized.ref 1;
    1.25 +val ambiguity_limit = Unsynchronized.ref 10;
    1.26  
    1.27  fun ambiguity_msg pos = "Parse error: ambiguous syntax" ^ Position.str_of pos;
    1.28  
    1.29 @@ -711,7 +711,7 @@
    1.30      unparse_typ: Proof.context -> typ -> Pretty.T,
    1.31      unparse_term: Proof.context -> term -> Pretty.T};
    1.32  
    1.33 -  val operations = ref (NONE: operations option);
    1.34 +  val operations = Unsynchronized.ref (NONE: operations option);
    1.35  
    1.36    fun operation which ctxt x =
    1.37      (case ! operations of