1.1 --- a/src/Pure/Syntax/parser.ML	Fri Jul 02 21:41:06 2010 +0200
     1.2 +++ b/src/Pure/Syntax/parser.ML	Fri Jul 02 21:48:54 2010 +0200
     1.3 @@ -8,9 +8,9 @@
     1.4  sig
     1.5    type gram
     1.6    val empty_gram: gram
     1.7 -  val extend_gram: gram -> Syn_Ext.xprod list -> gram
     1.8 +  val extend_gram: Syn_Ext.xprod list -> gram -> gram
     1.9    val make_gram: Syn_Ext.xprod list -> gram
    1.10 -  val merge_grams: gram -> gram -> gram
    1.11 +  val merge_gram: gram * gram -> gram
    1.12    val pretty_gram: gram -> Pretty.T list
    1.13    datatype parsetree =
    1.14      Node of string * parsetree list |
    1.15 @@ -435,76 +435,75 @@
    1.16  
    1.17  
    1.18  (*Add productions to a grammar*)
    1.19 -fun extend_gram gram [] = gram
    1.20 -  | extend_gram (Gram {nt_count, prod_count, tags, chains, lambdas, prods})
    1.21 -                xprods =
    1.22 -  let
    1.23 -    (*Get tag for existing nonterminal or create a new one*)
    1.24 -    fun get_tag nt_count tags nt =
    1.25 -      case Symtab.lookup tags nt of
    1.26 -        SOME tag => (nt_count, tags, tag)
    1.27 -      | NONE => (nt_count+1, Symtab.update_new (nt, nt_count) tags,
    1.28 -                 nt_count);
    1.29 +fun extend_gram [] gram = gram
    1.30 +  | extend_gram xprods (Gram {nt_count, prod_count, tags, chains, lambdas, prods}) =
    1.31 +    let
    1.32 +      (*Get tag for existing nonterminal or create a new one*)
    1.33 +      fun get_tag nt_count tags nt =
    1.34 +        case Symtab.lookup tags nt of
    1.35 +          SOME tag => (nt_count, tags, tag)
    1.36 +        | NONE => (nt_count+1, Symtab.update_new (nt, nt_count) tags,
    1.37 +                   nt_count);
    1.38  
    1.39 -    (*Convert symbols to the form used by the parser;
    1.40 -      delimiters and predefined terms are stored as terminals,
    1.41 -      nonterminals are converted to integer tags*)
    1.42 -    fun symb_of [] nt_count tags result = (nt_count, tags, rev result)
    1.43 -      | symb_of ((Syn_Ext.Delim s) :: ss) nt_count tags result =
    1.44 -          symb_of ss nt_count tags
    1.45 -            (Terminal (Lexicon.Token (Lexicon.Literal, s, Position.no_range)) :: result)
    1.46 -      | symb_of ((Syn_Ext.Argument (s, p)) :: ss) nt_count tags result =
    1.47 -          let
    1.48 -            val (nt_count', tags', new_symb) =
    1.49 -              case Lexicon.predef_term s of
    1.50 -                NONE =>
    1.51 -                  let val (nt_count', tags', s_tag) = get_tag nt_count tags s;
    1.52 -                  in (nt_count', tags', Nonterminal (s_tag, p)) end
    1.53 -              | SOME tk => (nt_count, tags, Terminal tk);
    1.54 -          in symb_of ss nt_count' tags' (new_symb :: result) end
    1.55 -      | symb_of (_ :: ss) nt_count tags result =
    1.56 -          symb_of ss nt_count tags result;
    1.57 +      (*Convert symbols to the form used by the parser;
    1.58 +        delimiters and predefined terms are stored as terminals,
    1.59 +        nonterminals are converted to integer tags*)
    1.60 +      fun symb_of [] nt_count tags result = (nt_count, tags, rev result)
    1.61 +        | symb_of ((Syn_Ext.Delim s) :: ss) nt_count tags result =
    1.62 +            symb_of ss nt_count tags
    1.63 +              (Terminal (Lexicon.Token (Lexicon.Literal, s, Position.no_range)) :: result)
    1.64 +        | symb_of ((Syn_Ext.Argument (s, p)) :: ss) nt_count tags result =
    1.65 +            let
    1.66 +              val (nt_count', tags', new_symb) =
    1.67 +                case Lexicon.predef_term s of
    1.68 +                  NONE =>
    1.69 +                    let val (nt_count', tags', s_tag) = get_tag nt_count tags s;
    1.70 +                    in (nt_count', tags', Nonterminal (s_tag, p)) end
    1.71 +                | SOME tk => (nt_count, tags, Terminal tk);
    1.72 +            in symb_of ss nt_count' tags' (new_symb :: result) end
    1.73 +        | symb_of (_ :: ss) nt_count tags result =
    1.74 +            symb_of ss nt_count tags result;
    1.75  
    1.76 -    (*Convert list of productions by invoking symb_of for each of them*)
    1.77 -    fun prod_of [] nt_count prod_count tags result =
    1.78 -          (nt_count, prod_count, tags, result)
    1.79 -      | prod_of ((Syn_Ext.XProd (lhs, xsymbs, const, pri)) :: ps)
    1.80 -                nt_count prod_count tags result =
    1.81 -        let val (nt_count', tags', lhs_tag) = get_tag nt_count tags lhs;
    1.82 +      (*Convert list of productions by invoking symb_of for each of them*)
    1.83 +      fun prod_of [] nt_count prod_count tags result =
    1.84 +            (nt_count, prod_count, tags, result)
    1.85 +        | prod_of ((Syn_Ext.XProd (lhs, xsymbs, const, pri)) :: ps)
    1.86 +                  nt_count prod_count tags result =
    1.87 +          let val (nt_count', tags', lhs_tag) = get_tag nt_count tags lhs;
    1.88  
    1.89 -            val (nt_count'', tags'', prods) =
    1.90 -              symb_of xsymbs nt_count' tags' [];
    1.91 -        in prod_of ps nt_count'' (prod_count+1) tags''
    1.92 -                   ((lhs_tag, (prods, const, pri)) :: result)
    1.93 -        end;
    1.94 +              val (nt_count'', tags'', prods) =
    1.95 +                symb_of xsymbs nt_count' tags' [];
    1.96 +          in prod_of ps nt_count'' (prod_count+1) tags''
    1.97 +                     ((lhs_tag, (prods, const, pri)) :: result)
    1.98 +          end;
    1.99  
   1.100 -    val (nt_count', prod_count', tags', xprods') =
   1.101 -      prod_of xprods nt_count prod_count tags [];
   1.102 +      val (nt_count', prod_count', tags', xprods') =
   1.103 +        prod_of xprods nt_count prod_count tags [];
   1.104  
   1.105 -    (*Copy array containing productions of old grammar;
   1.106 -      this has to be done to preserve the old grammar while being able
   1.107 -      to change the array's content*)
   1.108 -    val prods' =
   1.109 -      let fun get_prod i = if i < nt_count then Array.sub (prods, i)
   1.110 -                           else (([], []), []);
   1.111 -      in Array.tabulate (nt_count', get_prod) end;
   1.112 +      (*Copy array containing productions of old grammar;
   1.113 +        this has to be done to preserve the old grammar while being able
   1.114 +        to change the array's content*)
   1.115 +      val prods' =
   1.116 +        let fun get_prod i = if i < nt_count then Array.sub (prods, i)
   1.117 +                             else (([], []), []);
   1.118 +        in Array.tabulate (nt_count', get_prod) end;
   1.119  
   1.120 -    val fromto_chains = inverse_chains chains [];
   1.121 +      val fromto_chains = inverse_chains chains [];
   1.122  
   1.123 -    (*Add new productions to old ones*)
   1.124 -    val (fromto_chains', lambdas', _) =
   1.125 -      add_prods prods' fromto_chains lambdas NONE xprods';
   1.126 +      (*Add new productions to old ones*)
   1.127 +      val (fromto_chains', lambdas', _) =
   1.128 +        add_prods prods' fromto_chains lambdas NONE xprods';
   1.129  
   1.130 -    val chains' = inverse_chains fromto_chains' [];
   1.131 -  in Gram {nt_count = nt_count', prod_count = prod_count', tags = tags',
   1.132 -           chains = chains', lambdas = lambdas', prods = prods'}
   1.133 -  end;
   1.134 +      val chains' = inverse_chains fromto_chains' [];
   1.135 +    in Gram {nt_count = nt_count', prod_count = prod_count', tags = tags',
   1.136 +             chains = chains', lambdas = lambdas', prods = prods'}
   1.137 +    end;
   1.138  
   1.139 -val make_gram = extend_gram empty_gram;
   1.140 +fun make_gram xprods = extend_gram xprods empty_gram;
   1.141  
   1.142  
   1.143  (*Merge two grammars*)
   1.144 -fun merge_grams gram_a gram_b =
   1.145 +fun merge_gram (gram_a, gram_b) =
   1.146    let
   1.147      (*find out which grammar is bigger*)
   1.148      val (Gram {nt_count = nt_count1, prod_count = prod_count1, tags = tags1,
   1.149 @@ -811,7 +810,7 @@
   1.150      val start_tag =
   1.151        (case Symtab.lookup tags startsymbol of
   1.152          SOME tag => tag
   1.153 -      | NONE => error ("parse: Unknown startsymbol " ^ quote startsymbol));
   1.154 +      | NONE => error ("Inner syntax: unknown startsymbol " ^ quote startsymbol));
   1.155      val S0 = [(~1, 0, [], [Nonterminal (start_tag, 0), Terminal Lexicon.eof], "", 0)];
   1.156      val s = length indata + 1;
   1.157      val Estate = Array.array (s, []);
   1.158 @@ -829,7 +828,7 @@
   1.159        | SOME (Lexicon.Token (_, _, (_, end_pos))) => end_pos);
   1.160      val r =
   1.161        (case earley prods tags chains start (toks @ [Lexicon.mk_eof end_pos]) of
   1.162 -        [] => sys_error "parse: no parse trees"
   1.163 +        [] => raise Fail "no parse trees"
   1.164        | pts => pts);
   1.165    in r end;
   1.166  

     2.1 --- a/src/Pure/Syntax/syntax.ML	Fri Jul 02 21:41:06 2010 +0200
     2.2 +++ b/src/Pure/Syntax/syntax.ML	Fri Jul 02 21:48:54 2010 +0200
     2.3 @@ -297,7 +297,7 @@
     2.4      Syntax
     2.5      ({input = new_xprods @ input,
     2.6        lexicon = fold Scan.extend_lexicon (Syn_Ext.delims_of new_xprods) lexicon,
     2.7 -      gram = Parser.extend_gram gram new_xprods,
     2.8 +      gram = Parser.extend_gram new_xprods gram,
     2.9        consts = Library.merge (op =) (consts1, filter_out Lexicon.is_marked consts2),
    2.10        prmodes = insert (op =) mode (Library.merge (op =) (prmodes1, prmodes2)),
    2.11        parse_ast_trtab =
    2.12 @@ -362,7 +362,7 @@
    2.13      Syntax
    2.14      ({input = Library.merge (op =) (input1, input2),
    2.15        lexicon = Scan.merge_lexicons (lexicon1, lexicon2),
    2.16 -      gram = Parser.merge_grams gram1 gram2,
    2.17 +      gram = Parser.merge_gram (gram1, gram2),
    2.18        consts = sort_distinct string_ord (consts1 @ consts2),
    2.19        prmodes = Library.merge (op =) (prmodes1, prmodes2),
    2.20        parse_ast_trtab =