# HG changeset patch
# User wenzelm
# Date 1302278893 -7200
# Node ID 0f4372a2d2e4ac35155583cb9675c8d8416bec39
# Parent  6cca0343ea48909aa5ecb922ea67c582a73c1492
simplified Pure syntax bootstrap;

diff -r 6cca0343ea48 -r 0f4372a2d2e4 src/Pure/Syntax/syntax.ML
--- 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",
diff -r 6cca0343ea48 -r 0f4372a2d2e4 src/Pure/Syntax/syntax_ext.ML
--- 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;
diff -r 6cca0343ea48 -r 0f4372a2d2e4 src/Pure/Syntax/syntax_phases.ML
--- 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)
diff -r 6cca0343ea48 -r 0f4372a2d2e4 src/Pure/pure_thy.ML
--- 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 "_"),
diff -r 6cca0343ea48 -r 0f4372a2d2e4 src/Pure/sign.ML
--- 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