# HG changeset patch
# User wenzelm
# Date 1278100134 -7200
# Node ID d123b1e0885625b8eea8f256e73072f0d3bdb1a0
# Parent  ece640e48a6c06a2350440cc60bdba5ca38ff237
standard argument order;
tuned;

diff -r ece640e48a6c -r d123b1e08856 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Fri Jul 02 21:41:06 2010 +0200
+++ b/src/Pure/Syntax/parser.ML	Fri Jul 02 21:48:54 2010 +0200
@@ -8,9 +8,9 @@
 sig
   type gram
   val empty_gram: gram
-  val extend_gram: gram -> Syn_Ext.xprod list -> gram
+  val extend_gram: Syn_Ext.xprod list -> gram -> gram
   val make_gram: Syn_Ext.xprod list -> gram
-  val merge_grams: gram -> gram -> gram
+  val merge_gram: gram * gram -> gram
   val pretty_gram: gram -> Pretty.T list
   datatype parsetree =
     Node of string * parsetree list |
@@ -435,76 +435,75 @@
 
 
 (*Add productions to a grammar*)
-fun extend_gram gram [] = gram
-  | extend_gram (Gram {nt_count, prod_count, tags, chains, lambdas, prods})
-                xprods =
-  let
-    (*Get tag for existing nonterminal or create a new one*)
-    fun get_tag nt_count tags nt =
-      case Symtab.lookup tags nt of
-        SOME tag => (nt_count, tags, tag)
-      | NONE => (nt_count+1, Symtab.update_new (nt, nt_count) tags,
-                 nt_count);
+fun extend_gram [] gram = gram
+  | extend_gram xprods (Gram {nt_count, prod_count, tags, chains, lambdas, prods}) =
+    let
+      (*Get tag for existing nonterminal or create a new one*)
+      fun get_tag nt_count tags nt =
+        case Symtab.lookup tags nt of
+          SOME tag => (nt_count, tags, tag)
+        | NONE => (nt_count+1, Symtab.update_new (nt, nt_count) tags,
+                   nt_count);
 
-    (*Convert symbols to the form used by the parser;
-      delimiters and predefined terms are stored as terminals,
-      nonterminals are converted to integer tags*)
-    fun symb_of [] nt_count tags result = (nt_count, tags, rev result)
-      | symb_of ((Syn_Ext.Delim s) :: ss) nt_count tags result =
-          symb_of ss nt_count tags
-            (Terminal (Lexicon.Token (Lexicon.Literal, s, Position.no_range)) :: result)
-      | symb_of ((Syn_Ext.Argument (s, p)) :: ss) nt_count tags result =
-          let
-            val (nt_count', tags', new_symb) =
-              case Lexicon.predef_term s of
-                NONE =>
-                  let val (nt_count', tags', s_tag) = get_tag nt_count tags s;
-                  in (nt_count', tags', Nonterminal (s_tag, p)) end
-              | SOME tk => (nt_count, tags, Terminal tk);
-          in symb_of ss nt_count' tags' (new_symb :: result) end
-      | symb_of (_ :: ss) nt_count tags result =
-          symb_of ss nt_count tags result;
+      (*Convert symbols to the form used by the parser;
+        delimiters and predefined terms are stored as terminals,
+        nonterminals are converted to integer tags*)
+      fun symb_of [] nt_count tags result = (nt_count, tags, rev result)
+        | symb_of ((Syn_Ext.Delim s) :: ss) nt_count tags result =
+            symb_of ss nt_count tags
+              (Terminal (Lexicon.Token (Lexicon.Literal, s, Position.no_range)) :: result)
+        | symb_of ((Syn_Ext.Argument (s, p)) :: ss) nt_count tags result =
+            let
+              val (nt_count', tags', new_symb) =
+                case Lexicon.predef_term s of
+                  NONE =>
+                    let val (nt_count', tags', s_tag) = get_tag nt_count tags s;
+                    in (nt_count', tags', Nonterminal (s_tag, p)) end
+                | SOME tk => (nt_count, tags, Terminal tk);
+            in symb_of ss nt_count' tags' (new_symb :: result) end
+        | symb_of (_ :: ss) nt_count tags result =
+            symb_of ss nt_count tags result;
 
-    (*Convert list of productions by invoking symb_of for each of them*)
-    fun prod_of [] nt_count prod_count tags result =
-          (nt_count, prod_count, tags, result)
-      | prod_of ((Syn_Ext.XProd (lhs, xsymbs, const, pri)) :: ps)
-                nt_count prod_count tags result =
-        let val (nt_count', tags', lhs_tag) = get_tag nt_count tags lhs;
+      (*Convert list of productions by invoking symb_of for each of them*)
+      fun prod_of [] nt_count prod_count tags result =
+            (nt_count, prod_count, tags, result)
+        | prod_of ((Syn_Ext.XProd (lhs, xsymbs, const, pri)) :: ps)
+                  nt_count prod_count tags result =
+          let val (nt_count', tags', lhs_tag) = get_tag nt_count tags lhs;
 
-            val (nt_count'', tags'', prods) =
-              symb_of xsymbs nt_count' tags' [];
-        in prod_of ps nt_count'' (prod_count+1) tags''
-                   ((lhs_tag, (prods, const, pri)) :: result)
-        end;
+              val (nt_count'', tags'', prods) =
+                symb_of xsymbs nt_count' tags' [];
+          in prod_of ps nt_count'' (prod_count+1) tags''
+                     ((lhs_tag, (prods, const, pri)) :: result)
+          end;
 
-    val (nt_count', prod_count', tags', xprods') =
-      prod_of xprods nt_count prod_count tags [];
+      val (nt_count', prod_count', tags', xprods') =
+        prod_of xprods nt_count prod_count tags [];
 
-    (*Copy array containing productions of old grammar;
-      this has to be done to preserve the old grammar while being able
-      to change the array's content*)
-    val prods' =
-      let fun get_prod i = if i < nt_count then Array.sub (prods, i)
-                           else (([], []), []);
-      in Array.tabulate (nt_count', get_prod) end;
+      (*Copy array containing productions of old grammar;
+        this has to be done to preserve the old grammar while being able
+        to change the array's content*)
+      val prods' =
+        let fun get_prod i = if i < nt_count then Array.sub (prods, i)
+                             else (([], []), []);
+        in Array.tabulate (nt_count', get_prod) end;
 
-    val fromto_chains = inverse_chains chains [];
+      val fromto_chains = inverse_chains chains [];
 
-    (*Add new productions to old ones*)
-    val (fromto_chains', lambdas', _) =
-      add_prods prods' fromto_chains lambdas NONE xprods';
+      (*Add new productions to old ones*)
+      val (fromto_chains', lambdas', _) =
+        add_prods prods' fromto_chains lambdas NONE xprods';
 
-    val chains' = inverse_chains fromto_chains' [];
-  in Gram {nt_count = nt_count', prod_count = prod_count', tags = tags',
-           chains = chains', lambdas = lambdas', prods = prods'}
-  end;
+      val chains' = inverse_chains fromto_chains' [];
+    in Gram {nt_count = nt_count', prod_count = prod_count', tags = tags',
+             chains = chains', lambdas = lambdas', prods = prods'}
+    end;
 
-val make_gram = extend_gram empty_gram;
+fun make_gram xprods = extend_gram xprods empty_gram;
 
 
 (*Merge two grammars*)
-fun merge_grams gram_a gram_b =
+fun merge_gram (gram_a, gram_b) =
   let
     (*find out which grammar is bigger*)
     val (Gram {nt_count = nt_count1, prod_count = prod_count1, tags = tags1,
@@ -811,7 +810,7 @@
     val start_tag =
       (case Symtab.lookup tags startsymbol of
         SOME tag => tag
-      | NONE => error ("parse: Unknown startsymbol " ^ quote startsymbol));
+      | NONE => error ("Inner syntax: unknown startsymbol " ^ quote startsymbol));
     val S0 = [(~1, 0, [], [Nonterminal (start_tag, 0), Terminal Lexicon.eof], "", 0)];
     val s = length indata + 1;
     val Estate = Array.array (s, []);
@@ -829,7 +828,7 @@
       | SOME (Lexicon.Token (_, _, (_, end_pos))) => end_pos);
     val r =
       (case earley prods tags chains start (toks @ [Lexicon.mk_eof end_pos]) of
-        [] => sys_error "parse: no parse trees"
+        [] => raise Fail "no parse trees"
       | pts => pts);
   in r end;
 
diff -r ece640e48a6c -r d123b1e08856 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Fri Jul 02 21:41:06 2010 +0200
+++ b/src/Pure/Syntax/syntax.ML	Fri Jul 02 21:48:54 2010 +0200
@@ -297,7 +297,7 @@
     Syntax
     ({input = new_xprods @ input,
       lexicon = fold Scan.extend_lexicon (Syn_Ext.delims_of new_xprods) lexicon,
-      gram = Parser.extend_gram gram new_xprods,
+      gram = Parser.extend_gram new_xprods gram,
       consts = Library.merge (op =) (consts1, filter_out Lexicon.is_marked consts2),
       prmodes = insert (op =) mode (Library.merge (op =) (prmodes1, prmodes2)),
       parse_ast_trtab =
@@ -362,7 +362,7 @@
     Syntax
     ({input = Library.merge (op =) (input1, input2),
       lexicon = Scan.merge_lexicons (lexicon1, lexicon2),
-      gram = Parser.merge_grams gram1 gram2,
+      gram = Parser.merge_gram (gram1, gram2),
       consts = sort_distinct string_ord (consts1 @ consts2),
       prmodes = Library.merge (op =) (prmodes1, prmodes2),
       parse_ast_trtab =