provide structure Syntax early (before structure Type), back-patch check/uncheck later;
--- 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";
--- 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 =
--- 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;
--- 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;