adapted Scan.extend_lexicon/merge_lexicons;
authorwenzelm
Thu Aug 07 13:45:03 2008 +0200 (2008-08-07)
changeset 27768398c64b2acef
parent 27767 b52c0c81dcf3
child 27769 ad50c38ef842
adapted Scan.extend_lexicon/merge_lexicons;
src/Pure/Isar/outer_keyword.ML
src/Pure/Syntax/syntax.ML
     1.1 --- a/src/Pure/Isar/outer_keyword.ML	Thu Aug 07 13:44:56 2008 +0200
     1.2 +++ b/src/Pure/Isar/outer_keyword.ML	Thu Aug 07 13:45:03 2008 +0200
     1.3 @@ -154,11 +154,11 @@
     1.4  (* augment tables *)
     1.5  
     1.6  fun keyword name =
     1.7 - (change_lexicons (apfst (Scan.extend_lexicon [Symbol.explode name]));
     1.8 + (change_lexicons (apfst (Scan.extend_lexicon (Symbol.explode name)));
     1.9    Pretty.writeln (report_keyword name));
    1.10  
    1.11  fun command name kind =
    1.12 - (change_lexicons (apsnd (Scan.extend_lexicon [Symbol.explode name]));
    1.13 + (change_lexicons (apsnd (Scan.extend_lexicon (Symbol.explode name)));
    1.14    change_commands (Symtab.update (name, kind));
    1.15    Pretty.writeln (report_command (name, kind)));
    1.16  
     2.1 --- a/src/Pure/Syntax/syntax.ML	Thu Aug 07 13:44:56 2008 +0200
     2.2 +++ b/src/Pure/Syntax/syntax.ML	Thu Aug 07 13:45:03 2008 +0200
     2.3 @@ -296,7 +296,8 @@
     2.4    in
     2.5      Syntax
     2.6      ({input = input',
     2.7 -      lexicon = if changed then Scan.extend_lexicon (SynExt.delims_of xprods) lexicon else lexicon,
     2.8 +      lexicon =
     2.9 +        if changed then fold Scan.extend_lexicon (SynExt.delims_of xprods) lexicon else lexicon,
    2.10        gram = if changed then Parser.extend_gram gram xprods else gram,
    2.11        consts = Library.merge (op =) (consts1, filter_out NameSpace.is_qualified consts2),
    2.12        prmodes = insert (op =) mode (Library.merge (op =) (prmodes1, prmodes2)),
    2.13 @@ -361,7 +362,7 @@
    2.14    in
    2.15      Syntax
    2.16      ({input = Library.merge (op =) (input1, input2),
    2.17 -      lexicon = Scan.merge_lexicons lexicon1 lexicon2,
    2.18 +      lexicon = Scan.merge_lexicons (lexicon1, lexicon2),
    2.19        gram = Parser.merge_grams gram1 gram2,
    2.20        consts = sort_distinct string_ord (consts1 @ consts2),
    2.21        prmodes = Library.merge (op =) (prmodes1, prmodes2),
    2.22 @@ -464,7 +465,7 @@
    2.23    let
    2.24      val {lexicon, gram, parse_ast_trtab, ...} = tabs;
    2.25      val root' = if root <> "prop" andalso is_logtype root then SynExt.logic else root;
    2.26 -    val chars = Symbol.explode str;
    2.27 +    val chars = SymbolPos.explode (str, Position.none);
    2.28      val pts = Parser.parse gram root' (Lexicon.tokenize lexicon xids chars);
    2.29      val len = length pts;
    2.30