# HG changeset patch
# User wenzelm
# Date 1303076825 -7200
# Node ID dcd983ee2c29c60c6de5260ef21101268239870a
# Parent  309ec68442c6254c725173c0b12a4fe4f4360910
provide structure Syntax early (before structure Type), back-patch check/uncheck later;

diff -r 309ec68442c6 -r dcd983ee2c29 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sun Apr 17 21:42:47 2011 +0200
+++ b/src/Pure/ROOT.ML	Sun Apr 17 23:47:05 2011 +0200
@@ -103,24 +103,16 @@
 
 use "name.ML";
 use "term.ML";
-use "term_ord.ML";
-use "term_subst.ML";
-use "old_term.ML";
 use "General/pretty.ML";
 use "context.ML";
 use "config.ML";
 use "context_position.ML";
-use "General/name_space.ML";
-use "sorts.ML";
-use "type.ML";
-use "logic.ML";
 
 
 (* inner syntax *)
 
 use "Syntax/term_position.ML";
 use "Syntax/lexicon.ML";
-use "Syntax/simple_syntax.ML";
 use "Syntax/ast.ML";
 use "Syntax/syntax_ext.ML";
 use "Syntax/parser.ML";
@@ -132,6 +124,14 @@
 
 (* core of tactical proof system *)
 
+use "term_ord.ML";
+use "term_subst.ML";
+use "old_term.ML";
+use "General/name_space.ML";
+use "sorts.ML";
+use "type.ML";
+use "logic.ML";
+use "Syntax/simple_syntax.ML";
 use "net.ML";
 use "item_net.ML";
 use "envir.ML";
diff -r 309ec68442c6 -r dcd983ee2c29 src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Sun Apr 17 21:42:47 2011 +0200
+++ b/src/Pure/Syntax/printer.ML	Sun Apr 17 23:47:05 2011 +0200
@@ -36,12 +36,12 @@
   val pretty_term_ast: bool -> Proof.context -> prtabs ->
     (string -> Proof.context -> Ast.ast list -> Ast.ast) ->
     (string -> string -> Pretty.T option) ->
-    (string -> Markup.T list * xstring) ->
+    (string -> Markup.T list * string) ->
     Ast.ast -> Pretty.T list
   val pretty_typ_ast: Proof.context -> prtabs ->
     (string -> Proof.context -> Ast.ast list -> Ast.ast) ->
     (string -> string -> Pretty.T option) ->
-    (string -> Markup.T list * xstring) -> Ast.ast -> Pretty.T list
+    (string -> Markup.T list * string) -> Ast.ast -> Pretty.T list
 end;
 
 structure Printer: PRINTER =
diff -r 309ec68442c6 -r dcd983ee2c29 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Sun Apr 17 21:42:47 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML	Sun Apr 17 23:47:05 2011 +0200
@@ -10,6 +10,8 @@
   val const: string -> term
   val free: string -> term
   val var: indexname -> term
+  type operations
+  val install_operations: operations -> unit
   val root: string Config.T
   val positions_raw: Config.raw
   val positions: bool Config.T
@@ -28,14 +30,6 @@
   val unparse_arity: Proof.context -> arity -> Pretty.T
   val unparse_typ: Proof.context -> typ -> Pretty.T
   val unparse_term: Proof.context -> term -> Pretty.T
-  val install_operations:
-   {parse_sort: Proof.context -> string -> sort,
-    parse_typ: Proof.context -> string -> typ,
-    parse_term: Proof.context -> string -> term,
-    parse_prop: Proof.context -> string -> term,
-    unparse_sort: Proof.context -> sort -> Pretty.T,
-    unparse_typ: Proof.context -> typ -> Pretty.T,
-    unparse_term: Proof.context -> term -> Pretty.T} -> unit
   val print_checks: Proof.context -> unit
   val add_typ_check: int -> string ->
     (typ list -> Proof.context -> (typ list * Proof.context) option) ->
@@ -49,6 +43,10 @@
   val add_term_uncheck: int -> string ->
     (term list -> Proof.context -> (term list * Proof.context) option) ->
     Context.generic -> Context.generic
+  val typ_check: Proof.context -> typ list -> typ list
+  val term_check: Proof.context -> term list -> term list
+  val typ_uncheck: Proof.context -> typ list -> typ list
+  val term_uncheck: Proof.context -> term list -> term list
   val check_sort: Proof.context -> sort -> sort
   val check_typ: Proof.context -> typ -> typ
   val check_term: Proof.context -> term -> term
@@ -151,6 +149,31 @@
 
 (** inner syntax operations **)
 
+(* back-patched operations *)
+
+type operations =
+ {parse_sort: Proof.context -> string -> sort,
+  parse_typ: Proof.context -> string -> typ,
+  parse_term: Proof.context -> string -> term,
+  parse_prop: Proof.context -> string -> term,
+  unparse_sort: Proof.context -> sort -> Pretty.T,
+  unparse_typ: Proof.context -> typ -> Pretty.T,
+  unparse_term: Proof.context -> term -> Pretty.T,
+  check_typs: Proof.context -> typ list -> typ list,
+  check_terms: Proof.context -> term list -> term list,
+  check_props: Proof.context -> term list -> term list,
+  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;
+
+fun operation which ctxt x =
+  (case Single_Assignment.peek operations of
+    NONE => raise Fail "Inner syntax operations not installed"
+  | SOME ops => which ops ctxt x);
+
+
 (* configuration options *)
 
 val root = Config.string (Config.declare "syntax_root" (K (Config.String "any")));
@@ -191,26 +214,6 @@
     val _ = Context_Position.report ctxt pos markup;
   in (syms, pos) end;
 
-local
-
-type operations =
- {parse_sort: Proof.context -> string -> sort,
-  parse_typ: Proof.context -> string -> typ,
-  parse_term: Proof.context -> string -> term,
-  parse_prop: Proof.context -> string -> term,
-  unparse_sort: Proof.context -> sort -> Pretty.T,
-  unparse_typ: Proof.context -> typ -> Pretty.T,
-  unparse_term: Proof.context -> term -> Pretty.T};
-
-val operations: operations Single_Assignment.var = Single_Assignment.var "Syntax.operations";
-
-fun operation which ctxt x =
-  (case Single_Assignment.peek operations of
-    NONE => raise Fail "Inner syntax operations not installed"
-  | SOME ops => which ops ctxt x);
-
-in
-
 val parse_sort = operation #parse_sort;
 val parse_typ = operation #parse_typ;
 val parse_term = operation #parse_term;
@@ -219,10 +222,6 @@
 val unparse_typ = operation #unparse_typ;
 val unparse_term = operation #unparse_term;
 
-fun install_operations ops = Single_Assignment.assign operations ops;
-
-end;
-
 
 (* context-sensitive (un)checking *)
 
@@ -290,17 +289,22 @@
 fun add_typ_uncheck stage = gen_add apfst (stage, true);
 fun add_term_uncheck stage = gen_add apsnd (stage, true);
 
-val check_typs = gen_check fst false;
-val check_terms = gen_check snd false;
-fun check_props ctxt = map (Type.constraint propT) #> check_terms ctxt;
+val typ_check = gen_check fst false;
+val term_check = gen_check snd false;
+val typ_uncheck = gen_check fst true;
+val term_uncheck = gen_check snd true;
+
+val check_typs = operation #check_typs;
+val check_terms = operation #check_terms;
+val check_props = operation #check_props;
 
 val check_typ = singleton o check_typs;
 val check_term = singleton o check_terms;
 val check_prop = singleton o check_props;
 val check_sort = map_sort o check_typ;
 
-val uncheck_typs = gen_check fst true;
-val uncheck_terms = gen_check snd true;
+val uncheck_typs = operation #uncheck_typs;
+val uncheck_terms = operation #uncheck_terms;
 val uncheck_sort = map_sort o singleton o uncheck_typs;
 
 end;
diff -r 309ec68442c6 -r dcd983ee2c29 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Sun Apr 17 21:42:47 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Sun Apr 17 23:47:05 2011 +0200
@@ -702,6 +702,17 @@
 
 
 
+(** check/uncheck **)
+
+val check_typs = Syntax.typ_check;
+val check_terms = Syntax.term_check;
+fun check_props ctxt = map (Type.constraint propT) #> check_terms ctxt;
+
+val uncheck_typs = Syntax.typ_uncheck;
+val uncheck_terms = Syntax.term_uncheck;
+
+
+
 (** install operations **)
 
 val _ = Syntax.install_operations
@@ -711,6 +722,11 @@
    parse_prop = parse_term true,
    unparse_sort = unparse_sort,
    unparse_typ = unparse_typ,
-   unparse_term = unparse_term};
+   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;