src/Pure/Syntax/parser.ML
changeset 33063 4d462963a7db
parent 33042 ddf1f03a9ad9
child 33317 b4534348b8fd
equal deleted inserted replaced
33062:542b34b178ec 33063:4d462963a7db
   838   in r end;
   838   in r end;
   839 
   839 
   840 
   840 
   841 fun guess_infix_lr (Gram gram) c = (*based on educated guess*)
   841 fun guess_infix_lr (Gram gram) c = (*based on educated guess*)
   842   let
   842   let
   843     fun freeze a = map (curry Array.sub a) (0 upto Array.length a - 1);
   843     fun freeze a = map_range (curry Array.sub a) (Array.length a);
   844     val prods = maps snd (maps snd (freeze (#prods gram)));
   844     val prods = maps snd (maps snd (freeze (#prods gram)));
   845     fun guess (SOME ([Nonterminal (_, k), Terminal (Token (Literal, s, _)), Nonterminal (_, l)], _, j)) =
   845     fun guess (SOME ([Nonterminal (_, k), Terminal (Token (Literal, s, _)), Nonterminal (_, l)], _, j)) =
   846           if k = j andalso l = j + 1 then SOME (s, true, false, j)
   846           if k = j andalso l = j + 1 then SOME (s, true, false, j)
   847           else if k = j + 1 then if l = j then SOME (s, false, true, j)
   847           else if k = j + 1 then if l = j then SOME (s, false, true, j)
   848             else if l = j + 1 then SOME (s, false, false, j)
   848             else if l = j + 1 then SOME (s, false, false, j)