# HG changeset patch
# User wenzelm
# Date 1291484472 -3600
# Node ID 49765c1104d4267610e6532f276230ad30f6eb9c
# Parent  755f8fe7ced9f704c6307e330432e9de7bbef6cd
added Syntax.default_root;
simplified Syntax.parse operations;
clarified treatment of syntax root for translation rules -- refrain from logical_type replacement;
tuned error message;

diff -r 755f8fe7ced9 -r 49765c1104d4 NEWS
--- a/NEWS	Sat Dec 04 15:14:28 2010 +0100
+++ b/NEWS	Sat Dec 04 18:41:12 2010 +0100
@@ -585,6 +585,9 @@
 * Syntax.pretty_priority (default 0) configures the required priority
 of pretty-printed output and thus affects insertion of parentheses.
 
+* Syntax.default_root (default "any") configures the inner syntax
+category (nonterminal symbol) for parsing of terms.
+
 * Former exception Library.UnequalLengths now coincides with
 ListPair.UnequalLengths.
 
diff -r 755f8fe7ced9 -r 49765c1104d4 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sat Dec 04 15:14:28 2010 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sat Dec 04 18:41:12 2010 +0100
@@ -764,11 +764,19 @@
       if T' = propT then (Markup.prop, "proposition") else (Markup.term, "term");
     val (syms, pos) = Syntax.parse_token ctxt markup text;
 
+    val default_root = Config.get ctxt Syntax.default_root;
+    val root =
+      (case T' of
+        Type (c, _) =>
+          if c <> "prop" andalso Type.is_logtype (tsig_of ctxt) c
+          then default_root else c
+      | _ => default_root);
+
     fun check t = (Syntax.check_term ctxt (Type.constraint T' t); NONE)
       handle ERROR msg => SOME msg;
     val t =
       Syntax.standard_parse_term check get_sort map_const map_free
-        ctxt (Type.is_logtype (tsig_of ctxt)) (syn_of ctxt) T' (syms, pos)
+        ctxt (syn_of ctxt) root (syms, pos)
       handle ERROR msg => parse_failed ctxt pos msg kind;
   in t end;
 
diff -r 755f8fe7ced9 -r 49765c1104d4 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Sat Dec 04 15:14:28 2010 +0100
+++ b/src/Pure/Syntax/parser.ML	Sat Dec 04 18:41:12 2010 +0100
@@ -841,7 +841,7 @@
     val start_tag =
       (case Symtab.lookup tags startsymbol of
         SOME tag => tag
-      | NONE => error ("Inner syntax: unknown startsymbol " ^ quote startsymbol));
+      | NONE => error ("Inner syntax: bad grammar root symbol " ^ quote startsymbol));
     val S0 = [(~1, 0, [], [Nonterminal (start_tag, 0), Terminal Lexicon.eof], "", 0)];
     val s = length indata + 1;
     val Estate = Array.array (s, []);
diff -r 755f8fe7ced9 -r 49765c1104d4 src/Pure/Syntax/syn_ext.ML
--- a/src/Pure/Syntax/syn_ext.ML	Sat Dec 04 15:14:28 2010 +0100
+++ b/src/Pure/Syntax/syn_ext.ML	Sat Dec 04 18:41:12 2010 +0100
@@ -10,6 +10,7 @@
   val constrainC: string
   val typeT: typ
   val spropT: typ
+  val default_root: string Config.T
   val max_pri: int
   val stamp_trfun: stamp -> string * 'a -> string * ('a * stamp)
   val mk_trfun: string * 'a -> string * ('a * stamp)
@@ -112,6 +113,9 @@
 val any = "any";
 val anyT = Type (any, []);
 
+val default_root =
+  Config.string (Config.declare "Syntax.default_root" (K (Config.String any)));
+
 
 
 (** datatype xprod **)
diff -r 755f8fe7ced9 -r 49765c1104d4 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Sat Dec 04 15:14:28 2010 +0100
+++ b/src/Pure/Syntax/syntax.ML	Sat Dec 04 18:41:12 2010 +0100
@@ -117,7 +117,7 @@
   val standard_parse_term: (term -> string option) ->
     (((string * int) * sort) list -> string * int -> Term.sort) ->
     (string -> bool * string) -> (string -> string option) -> Proof.context ->
-    (string -> bool) -> syntax -> typ -> Symbol_Pos.T list * Position.T -> term
+    syntax -> string -> Symbol_Pos.T list * Position.T -> term
   val standard_parse_typ: Proof.context -> syntax ->
     ((indexname * sort) list -> indexname -> sort) -> Symbol_Pos.T list * Position.T -> typ
   val standard_parse_sort: Proof.context -> syntax -> Symbol_Pos.T list * Position.T -> sort
@@ -149,10 +149,8 @@
   val update_type_gram: bool -> mode -> (string * typ * mixfix) list -> syntax -> syntax
   val update_const_gram: bool -> (string -> bool) ->
     mode -> (string * typ * mixfix) list -> syntax -> syntax
-  val update_trrules: Proof.context -> (string -> bool) -> syntax ->
-    (string * string) trrule list -> syntax -> syntax
-  val remove_trrules: Proof.context -> (string -> bool) -> syntax ->
-    (string * string) trrule list -> syntax -> syntax
+  val update_trrules: Proof.context -> syntax -> (string * string) trrule list -> syntax -> syntax
+  val remove_trrules: Proof.context -> syntax -> (string * string) trrule list -> syntax -> syntax
   val update_trrules_i: ast trrule list -> syntax -> syntax
   val remove_trrules_i: ast trrule list -> syntax -> syntax
 end;
@@ -702,14 +700,13 @@
 
 fun ambiguity_msg pos = "Parse error: ambiguous syntax" ^ Position.str_of pos;
 
-fun read_asts ctxt is_logtype (Syntax (tabs, _)) xids root (syms, pos) =
+fun read_asts ctxt (Syntax (tabs, _)) xids root (syms, pos) =
   let
     val {lexicon, gram, parse_ast_trtab, ...} = tabs;
     val toks = Lexicon.tokenize lexicon xids syms;
     val _ = List.app (Lexicon.report_token ctxt) toks;
 
-    val root' = if root <> "prop" andalso is_logtype root then Syn_Ext.logic else root;
-    val pts = Parser.parse ctxt gram root' (filter Lexicon.is_proper toks)
+    val pts = Parser.parse ctxt gram root (filter Lexicon.is_proper toks)
       handle ERROR msg =>
         error (msg ^
           implode (map (Markup.markup Markup.report o Lexicon.reported_token_range ctxt) toks));
@@ -733,10 +730,10 @@
 
 (* read *)
 
-fun read ctxt is_logtype (syn as Syntax (tabs, _)) ty inp =
+fun read ctxt (syn as Syntax (tabs, _)) root inp =
   let
     val {parse_ruletab, parse_trtab, ...} = tabs;
-    val asts = read_asts ctxt is_logtype syn false (Syn_Ext.typ_to_nonterm ty) inp;
+    val asts = read_asts ctxt syn false root inp;
   in
     Syn_Trans.asts_to_terms ctxt (lookup_tr parse_trtab)
       (map (Ast.normalize_ast (Symtab.lookup_list parse_ruletab)) asts)
@@ -778,8 +775,8 @@
             map show_term (take limit results)))
       end;
 
-fun standard_parse_term check get_sort map_const map_free ctxt is_logtype syn ty (syms, pos) =
-  read ctxt is_logtype syn ty (syms, pos)
+fun standard_parse_term check get_sort map_const map_free ctxt syn root (syms, pos) =
+  read ctxt syn root (syms, pos)
   |> map (Type_Ext.decode_term get_sort map_const map_free)
   |> disambig ctxt check;
 
@@ -787,7 +784,7 @@
 (* read types *)
 
 fun standard_parse_typ ctxt syn get_sort (syms, pos) =
-  (case read ctxt (K false) syn Syn_Ext.typeT (syms, pos) of
+  (case read ctxt syn (Syn_Ext.typ_to_nonterm Syn_Ext.typeT) (syms, pos) of
     [t] => Type_Ext.typ_of_term (get_sort (Type_Ext.term_sorts t)) t
   | _ => error (ambiguity_msg pos));
 
@@ -795,7 +792,7 @@
 (* read sorts *)
 
 fun standard_parse_sort ctxt syn (syms, pos) =
-  (case read ctxt (K false) syn Type_Ext.sortT (syms, pos) of
+  (case read ctxt syn (Syn_Ext.typ_to_nonterm Type_Ext.sortT) (syms, pos) of
     [t] => Type_Ext.sort_of_term t
   | _ => error (ambiguity_msg pos));
 
@@ -832,7 +829,7 @@
         Ast.str_of_ast lhs ^ "  ->  " ^ Ast.str_of_ast rhs)
   | NONE => rule);
 
-fun read_pattern ctxt is_logtype syn (root, str) =
+fun read_pattern ctxt syn (root, str) =
   let
     fun constify (ast as Ast.Constant _) = ast
       | constify (ast as Ast.Variable x) =
@@ -842,7 +839,7 @@
 
     val (syms, pos) = read_token str;
   in
-    (case read_asts ctxt is_logtype syn true root (syms, pos) of
+    (case read_asts ctxt syn true root (syms, pos) of
       [ast] => constify ast
     | _ => error (ambiguity_msg pos))
   end;
@@ -857,8 +854,7 @@
 
 val cert_rules = prep_rules I;
 
-fun read_rules ctxt is_logtype syn =
-  prep_rules (read_pattern ctxt is_logtype syn);
+fun read_rules ctxt syn = prep_rules (read_pattern ctxt syn);
 
 end;
 
@@ -909,11 +905,11 @@
 fun update_const_gram add is_logtype prmode decls =
   (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_consts is_logtype decls);
 
-fun update_trrules ctxt is_logtype syn =
-  ext_syntax Syn_Ext.syn_ext_rules o read_rules ctxt is_logtype syn;
+fun update_trrules ctxt syn =
+  ext_syntax Syn_Ext.syn_ext_rules o read_rules ctxt syn;
 
-fun remove_trrules ctxt is_logtype syn =
-  remove_syntax mode_default o Syn_Ext.syn_ext_rules o read_rules ctxt is_logtype syn;
+fun remove_trrules ctxt syn =
+  remove_syntax mode_default o Syn_Ext.syn_ext_rules o read_rules ctxt syn;
 
 val update_trrules_i = ext_syntax Syn_Ext.syn_ext_rules o cert_rules;
 val remove_trrules_i = remove_syntax mode_default o Syn_Ext.syn_ext_rules o cert_rules;
diff -r 755f8fe7ced9 -r 49765c1104d4 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Sat Dec 04 15:14:28 2010 +0100
+++ b/src/Pure/sign.ML	Sat Dec 04 18:41:12 2010 +0100
@@ -499,7 +499,7 @@
 
 fun gen_trrules f args thy = thy |> map_syn (fn syn =>
   let val rules = map (Syntax.map_trrule (apfst (intern_type thy))) args
-  in f (ProofContext.init_global thy) (is_logtype thy) syn rules syn end);
+  in f (ProofContext.init_global thy) syn rules syn end);
 
 val add_trrules = gen_trrules Syntax.update_trrules;
 val del_trrules = gen_trrules Syntax.remove_trrules;