--- a/src/Pure/Syntax/syntax.ML Fri Apr 08 17:45:37 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML Fri Apr 08 18:08:13 2011 +0200
@@ -111,8 +111,9 @@
type mode
val mode_default: mode
val mode_input: mode
+ val empty_syntax: syntax
val merge_syntaxes: syntax -> syntax -> syntax
- val basic_syntax: syntax
+ val token_markers: string list
val basic_nonterms: string list
val print_gram: syntax -> unit
val print_trans: syntax -> unit
@@ -599,7 +600,8 @@
(* basic syntax *)
-val basic_syntax = update_syntax mode_default Syntax_Ext.pure_ext empty_syntax;
+val token_markers =
+ ["_tfree", "_tvar", "_free", "_bound", "_var", "_numeral", "_inner_string"];
val basic_nonterms =
(Lexicon.terminals @ ["logic", "type", "types", "sort", "classes",
--- a/src/Pure/Syntax/syntax_ext.ML Fri Apr 08 17:45:37 2011 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML Fri Apr 08 18:08:13 2011 +0200
@@ -59,8 +59,6 @@
val stamp_trfun: stamp -> string * 'a -> string * ('a * stamp)
val mk_trfun: string * 'a -> string * ('a * stamp)
val eq_trfun: ('a * stamp) * ('a * stamp) -> bool
- val token_markers: string list
- val pure_ext: syn_ext
end;
structure Syntax_Ext: SYNTAX_EXT =
@@ -335,24 +333,4 @@
fun mk_trfun tr = stamp_trfun (stamp ()) tr;
fun eq_trfun ((_, s1: stamp), (_, s2)) = s1 = s2;
-
-(* pure_ext *)
-
-val token_markers =
- ["_tfree", "_tvar", "_free", "_bound", "_var", "_numeral", "_inner_string"];
-
-val typ = Simple_Syntax.read_typ;
-
-val pure_ext = syn_ext' (K false)
- [Mfix ("_", typ "prop' => prop", "", [0], 0),
- Mfix ("_", typ "logic => any", "", [0], 0),
- Mfix ("_", typ "prop' => any", "", [0], 0),
- Mfix ("'(_')", typ "logic => logic", "", [0], max_pri),
- Mfix ("'(_')", typ "prop' => prop'", "", [0], max_pri),
- Mfix ("_::_", typ "logic => type => logic", "_constrain", [4, 0], 3),
- Mfix ("_::_", typ "prop' => type => prop'", "_constrain", [4, 0], 3)]
- token_markers
- ([], [], [], [])
- ([], []);
-
end;
--- a/src/Pure/Syntax/syntax_phases.ML Fri Apr 08 17:45:37 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML Fri Apr 08 18:08:13 2011 +0200
@@ -491,7 +491,7 @@
val {structs, fixes} = idents;
fun mark_atoms ((t as Const (c, _)) $ u) =
- if member (op =) Syntax_Ext.token_markers c
+ if member (op =) Syntax.token_markers c
then t $ u else mark_atoms t $ mark_atoms u
| mark_atoms (t $ u) = mark_atoms t $ mark_atoms u
| mark_atoms (Abs (x, T, t)) = Abs (x, T, mark_atoms t)
--- a/src/Pure/pure_thy.ML Fri Apr 08 17:45:37 2011 +0200
+++ b/src/Pure/pure_thy.ML Fri Apr 08 18:08:13 2011 +0200
@@ -61,8 +61,16 @@
(Binding.name "itself", 1, NoSyn),
(Binding.name "dummy", 0, NoSyn)]
#> Sign.add_nonterminals (map Binding.name Syntax.basic_nonterms)
+ #> Sign.add_syntax_i (map (fn x => (x, typ "'a", NoSyn)) Syntax.token_markers)
#> Sign.add_syntax_i
- [("", typ "tid => type", Delimfix "_"),
+ [("", typ "prop' => prop", Delimfix "_"),
+ ("", typ "logic => any", Delimfix "_"),
+ ("", typ "prop' => any", Delimfix "_"),
+ ("", typ "logic => logic", Delimfix "'(_')"),
+ ("", typ "prop' => prop'", Delimfix "'(_')"),
+ ("_constrain", typ "logic => type => logic", Mixfix ("_::_", [4, 0], 3)),
+ ("_constrain", typ "prop' => type => prop'", Mixfix ("_::_", [4, 0], 3)),
+ ("", typ "tid => type", Delimfix "_"),
("", typ "tvar => type", Delimfix "_"),
("", typ "type_name => type", Delimfix "_"),
("_type_name", typ "id => type_name", Delimfix "_"),
--- a/src/Pure/sign.ML Fri Apr 08 17:45:37 2011 +0200
+++ b/src/Pure/sign.ML Fri Apr 08 18:08:13 2011 +0200
@@ -140,7 +140,7 @@
make_sign (Name_Space.default_naming, syn, tsig, consts);
val empty =
- make_sign (Name_Space.default_naming, Syntax.basic_syntax, Type.empty_tsig, Consts.empty);
+ make_sign (Name_Space.default_naming, Syntax.empty_syntax, Type.empty_tsig, Consts.empty);
fun merge pp (sign1, sign2) =
let