# HG changeset patch
# User wenzelm
# Date 1460023682 -7200
# Node ID 8093203f0b895f1e3de529e51ec8c1423a1bb745
# Parent  4ee9c2be4383e8ff65a497016c775833ee232f65
prefer regular context update, to allow continuous editing of Pure;

diff -r 4ee9c2be4383 -r 8093203f0b89 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Thu Apr 07 11:17:57 2016 +0200
+++ b/src/Pure/Syntax/syntax.ML	Thu Apr 07 12:08:02 2016 +0200
@@ -8,7 +8,7 @@
 signature SYNTAX =
 sig
   type operations
-  val install_operations: operations -> unit
+  val install_operations: operations -> theory -> theory
   val root: string Config.T
   val ambiguity_warning_raw: Config.raw
   val ambiguity_warning: bool Config.T
@@ -123,7 +123,7 @@
 
 (** inner syntax operations **)
 
-(* back-patched operations *)
+(* operations *)
 
 type operations =
  {parse_sort: Proof.context -> string -> sort,
@@ -139,11 +139,21 @@
   uncheck_typs: Proof.context -> typ list -> typ list,
   uncheck_terms: Proof.context -> term list -> term list};
 
-val operations: operations Single_Assignment.var = Single_Assignment.var "Syntax.operations";
-fun install_operations ops = Single_Assignment.assign operations ops;
+structure Operations = Theory_Data
+(
+  type T = operations option;
+  val empty = NONE;
+  val extend = I;
+  val merge = merge_options;
+);
+
+fun install_operations ops =
+  Operations.map
+    (fn NONE => SOME ops
+      | SOME _ => raise Fail "Inner syntax operations already installed");
 
 fun operation which ctxt x =
-  (case Single_Assignment.peek operations of
+  (case Operations.get (Proof_Context.theory_of ctxt) of
     NONE => raise Fail "Inner syntax operations not installed"
   | SOME ops => which ops ctxt x);
 
diff -r 4ee9c2be4383 -r 8093203f0b89 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Thu Apr 07 11:17:57 2016 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Thu Apr 07 12:08:02 2016 +0200
@@ -983,18 +983,20 @@
 
 (** install operations **)
 
-val _ = Syntax.install_operations
-  {parse_sort = parse_sort,
-   parse_typ = parse_typ,
-   parse_term = parse_term false,
-   parse_prop = parse_term true,
-   unparse_sort = unparse_sort,
-   unparse_typ = unparse_typ,
-   unparse_term = unparse_term,
-   check_typs = check_typs,
-   check_terms = check_terms,
-   check_props = check_props,
-   uncheck_typs = uncheck_typs,
-   uncheck_terms = uncheck_terms};
+val _ =
+  Theory.setup
+   (Syntax.install_operations
+     {parse_sort = parse_sort,
+      parse_typ = parse_typ,
+      parse_term = parse_term false,
+      parse_prop = parse_term true,
+      unparse_sort = unparse_sort,
+      unparse_typ = unparse_typ,
+      unparse_term = unparse_term,
+      check_typs = check_typs,
+      check_terms = check_terms,
+      check_props = check_props,
+      uncheck_typs = uncheck_typs,
+      uncheck_terms = uncheck_terms});
 
 end;
diff -r 4ee9c2be4383 -r 8093203f0b89 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Thu Apr 07 11:17:57 2016 +0200
+++ b/src/Pure/axclass.ML	Thu Apr 07 12:08:02 2016 +0200
@@ -261,12 +261,13 @@
     else SOME (map_proven_arities (K arities') thy)
   end;
 
-val _ = Theory.setup
-  (Theory.at_begin complete_classrels #> Theory.at_begin complete_arities);
-
-val _ = Proofterm.install_axclass_proofs
-  {classrel_proof = Thm.proof_of oo the_classrel,
-   arity_proof = Thm.proof_of oo the_arity};
+val _ =
+  Theory.setup
+   (Theory.at_begin complete_classrels #>
+    Theory.at_begin complete_arities #>
+    Proofterm.install_axclass_proofs
+     {classrel_proof = Thm.proof_of oo the_classrel,
+      arity_proof = Thm.proof_of oo the_arity});
 
 
 (* maintain instance parameters *)
diff -r 4ee9c2be4383 -r 8093203f0b89 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Thu Apr 07 11:17:57 2016 +0200
+++ b/src/Pure/proofterm.ML	Thu Apr 07 12:08:02 2016 +0200
@@ -127,7 +127,7 @@
   val of_sort_proof: theory -> (typ * class -> proof) -> typ * sort -> proof list
   val install_axclass_proofs:
    {classrel_proof: theory -> class * class -> proof,
-    arity_proof: theory -> string * sort list * class -> proof} -> unit
+    arity_proof: theory -> string * sort list * class -> proof} -> theory -> theory
   val axm_proof: string -> term -> proof
   val oracle_proof: string -> term -> oracle * proof
 
@@ -1027,20 +1027,28 @@
  {classrel_proof: theory -> class * class -> proof,
   arity_proof: theory -> string * sort list * class -> proof};
 
-val axclass_proofs: axclass_proofs Single_Assignment.var =
-  Single_Assignment.var "Proofterm.axclass_proofs";
+structure Axclass_Proofs = Theory_Data
+(
+  type T = axclass_proofs option;
+  val empty = NONE;
+  val extend = I;
+  val merge = merge_options;
+);
 
-fun axclass_proof which thy x =
-  (case Single_Assignment.peek axclass_proofs of
+fun the_axclass_proofs which thy x =
+  (case Axclass_Proofs.get thy of
     NONE => raise Fail "Axclass proof operations not installed"
-  | SOME prfs => which prfs thy x);
+  | SOME proofs => which proofs thy x);
 
 in
 
-val classrel_proof = axclass_proof #classrel_proof;
-val arity_proof = axclass_proof #arity_proof;
+val classrel_proof = the_axclass_proofs #classrel_proof;
+val arity_proof = the_axclass_proofs #arity_proof;
 
-fun install_axclass_proofs prfs = Single_Assignment.assign axclass_proofs prfs;
+fun install_axclass_proofs proofs =
+  Axclass_Proofs.map
+    (fn NONE => SOME proofs
+      | SOME _ => raise Fail "Axclass proof operations already installed");
 
 end;