back-patching via Single_Assignment.var;
authorwenzelm
Sat May 08 14:41:23 2010 +0200 (2010-05-08)
changeset 36739e9401d2efc5f
parent 36738 dce592144219
child 36740 6248aa22c694
back-patching via Single_Assignment.var;
src/Pure/Syntax/syntax.ML
     1.1 --- a/src/Pure/Syntax/syntax.ML	Fri May 07 23:44:10 2010 +0200
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Sat May 08 14:41:23 2010 +0200
     1.3 @@ -698,21 +698,23 @@
     1.4    in (syms, pos) end;
     1.5  
     1.6  local
     1.7 -  type operations =
     1.8 -   {parse_sort: Proof.context -> string -> sort,
     1.9 -    parse_typ: Proof.context -> string -> typ,
    1.10 -    parse_term: Proof.context -> string -> term,
    1.11 -    parse_prop: Proof.context -> string -> term,
    1.12 -    unparse_sort: Proof.context -> sort -> Pretty.T,
    1.13 -    unparse_typ: Proof.context -> typ -> Pretty.T,
    1.14 -    unparse_term: Proof.context -> term -> Pretty.T};
    1.15  
    1.16 -  val operations = Unsynchronized.ref (NONE: operations option);
    1.17 +type operations =
    1.18 + {parse_sort: Proof.context -> string -> sort,
    1.19 +  parse_typ: Proof.context -> string -> typ,
    1.20 +  parse_term: Proof.context -> string -> term,
    1.21 +  parse_prop: Proof.context -> string -> term,
    1.22 +  unparse_sort: Proof.context -> sort -> Pretty.T,
    1.23 +  unparse_typ: Proof.context -> typ -> Pretty.T,
    1.24 +  unparse_term: Proof.context -> term -> Pretty.T};
    1.25  
    1.26 -  fun operation which ctxt x =
    1.27 -    (case ! operations of
    1.28 -      NONE => error "Inner syntax operations not yet installed"
    1.29 -    | SOME ops => which ops ctxt x);
    1.30 +val operations: operations Single_Assignment.var = Single_Assignment.var "Syntax.operations";
    1.31 +
    1.32 +fun operation which ctxt x =
    1.33 +  (case Single_Assignment.peek operations of
    1.34 +    NONE => raise Fail "Inner syntax operations not installed"
    1.35 +  | SOME ops => which ops ctxt x);
    1.36 +
    1.37  in
    1.38  
    1.39  val parse_sort = operation #parse_sort;
    1.40 @@ -723,9 +725,7 @@
    1.41  val unparse_typ = operation #unparse_typ;
    1.42  val unparse_term = operation #unparse_term;
    1.43  
    1.44 -fun install_operations ops = CRITICAL (fn () =>
    1.45 -  if is_some (! operations) then error "Inner syntax operations already installed"
    1.46 -  else operations := SOME ops);
    1.47 +fun install_operations ops = Single_Assignment.assign operations ops;
    1.48  
    1.49  end;
    1.50