# HG changeset patch
# User wenzelm
# Date 754653847 -3600
# Node ID ab0f93a291b54821ac53b373f07e1f79ab4427ba
# Parent  590c9d1e0d73dd1addc639247037d63e230e0e36
*** empty log message ***

diff -r 590c9d1e0d73 -r ab0f93a291b5 src/Pure/Syntax/extension.ML
--- a/src/Pure/Syntax/extension.ML	Tue Nov 30 10:55:43 1993 +0100
+++ b/src/Pure/Syntax/extension.ML	Tue Nov 30 11:04:07 1993 +0100
@@ -3,10 +3,6 @@
     Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
 
 External grammar definition (internal interface).
-
-TODO:
-  ext = {roots, mfix, extra_consts} | {.._translation} | {.._rules} (?)
-  extend_xgram: move '.. \\ roots1' to Syntax.extend_tables (no?)
 *)
 
 signature EXTENSION0 =
@@ -83,21 +79,36 @@
 
 (* ext_components *)
 
-fun ext_components (Ext ext) =
-      {roots = #roots ext, mfix = #mfix ext, extra_consts = #extra_consts ext,
+fun ext_components (Ext ext) = {
+      roots = #roots ext,
+      mfix = #mfix ext,
+      extra_consts = #extra_consts ext,
       parse_ast_translation = #parse_ast_translation ext,
+      parse_rules = [],
       parse_translation = #parse_translation ext,
       print_translation = #print_translation ext,
-      print_ast_translation = #print_ast_translation ext,
-      parse_rules = [], print_rules = []}
-  | ext_components (ExtRules {parse_rules, print_rules}) =
-      {parse_rules = parse_rules, print_rules = print_rules, roots = [], mfix = [],
-      extra_consts = [], parse_ast_translation = [], parse_translation = [],
-      print_translation = [], print_ast_translation = []}
-  | ext_components (ExtRoots roots) =
-      {roots = roots, mfix = [], extra_consts = [], parse_ast_translation = [],
-      parse_rules = [], parse_translation = [], print_translation = [],
-      print_rules = [], print_ast_translation = []};
+      print_rules = [],
+      print_ast_translation = #print_ast_translation ext}
+  | ext_components (ExtRules {parse_rules, print_rules}) = {
+      roots = [],
+      mfix = [],
+      extra_consts = [],
+      parse_ast_translation = [],
+      parse_rules = parse_rules,
+      parse_translation = [],
+      print_translation = [],
+      print_rules = print_rules,
+      print_ast_translation = []}
+  | ext_components (ExtRoots roots) = {
+      roots = roots,
+      mfix = [],
+      extra_consts = [],
+      parse_ast_translation = [],
+      parse_rules = [],
+      parse_translation = [],
+      print_translation = [],
+      print_rules = [],
+      print_ast_translation = []};
 
 
 (* empty_xgram *)
diff -r 590c9d1e0d73 -r ab0f93a291b5 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Tue Nov 30 10:55:43 1993 +0100
+++ b/src/Pure/Syntax/syntax.ML	Tue Nov 30 11:04:07 1993 +0100
@@ -110,12 +110,12 @@
 
 (* empty_tables *)
 
+(*(* FIXME *)
 val empty_tables =
   Tabs {
     lexicon = empty_lexicon,
     roots = [],
-    (* gram = empty_gram, *)    (* FIXME *)
-    gram = mk_gram [] [],       (* FIXME *)
+    gram = empty_gram,
     consts = [],
     parse_ast_trtab = Symtab.null,
     parse_ruletab = Symtab.null,
@@ -123,6 +123,7 @@
     print_trtab = Symtab.null,
     print_ruletab = Symtab.null,
     prtab = empty_prtab};
+*)
 
 
 (* extend_tables *)
@@ -158,6 +159,7 @@
 
 (* mk_tables *)
 
+(* FIXME *)
 (* val mk_tables = extend_tables empty_tables; *)
 
 (* FIXME *)
@@ -426,7 +428,7 @@
 val type_syn = mk_syntax (ref (ExtGG (ref EmptyGG, type_ext)));
 
 
-(* extend *)  (* FIXME *) (* FIXME check *)
+(* extend *)  (* FIXME *)
 
 fun old_extend syn read_ty (roots, xconsts, sext) =
   let
diff -r 590c9d1e0d73 -r ab0f93a291b5 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Tue Nov 30 10:55:43 1993 +0100
+++ b/src/Pure/sign.ML	Tue Nov 30 11:04:07 1993 +0100
@@ -132,12 +132,6 @@
     (*read and check the type mentioned in a const declaration; zero type var
       indices because type inference requires it*)
 
-    (* FIXME bug / feature: varifyT'ed TFrees may clash with user specified
-      TVars e.g. foo :: "'a => ?'a" *)
-    (* FIXME if user supplied TVars were disallowed, zero_tvar_indices would
-      become obsolete *)
-    (* FIXME disallow "" as const name *)
-
     fun read_consts tsg sy (cs, s) =
       let val ty = zero_tvar_indices (Type.varifyT (read_typ tsg sy s));
       in
@@ -164,7 +158,6 @@
 
     val const_decs' =
       map (read_consts tsig' syn') (Syntax.constants sext @ const_decs);
-                    (* FIXME ^^^^ should be syn *)
   in
     Sg {
       tsig = tsig',
@@ -191,7 +184,7 @@
   (Syntax.syntax_types, 0)],
  [(["fun"],  ([["logic"], ["logic"]], "logic")),
   (["prop"], ([], "logic"))],
- [([Syntax.constrainC], "'a::logic => 'a")],  (* FIXME replace logic by {} (?) *)
+ [([Syntax.constrainC], "'a::logic => 'a")],
  Some Syntax.pure_sext);