# HG changeset patch
# User wenzelm
# Date 1218109503 -7200
# Node ID 398c64b2acef2c6a901ae038486eed2effa7e46b
# Parent  b52c0c81dcf334548241af6e1e9b189693d3f04b
adapted Scan.extend_lexicon/merge_lexicons;

diff -r b52c0c81dcf3 -r 398c64b2acef src/Pure/Isar/outer_keyword.ML
--- a/src/Pure/Isar/outer_keyword.ML	Thu Aug 07 13:44:56 2008 +0200
+++ b/src/Pure/Isar/outer_keyword.ML	Thu Aug 07 13:45:03 2008 +0200
@@ -154,11 +154,11 @@
 (* augment tables *)
 
 fun keyword name =
- (change_lexicons (apfst (Scan.extend_lexicon [Symbol.explode name]));
+ (change_lexicons (apfst (Scan.extend_lexicon (Symbol.explode name)));
   Pretty.writeln (report_keyword name));
 
 fun command name kind =
- (change_lexicons (apsnd (Scan.extend_lexicon [Symbol.explode name]));
+ (change_lexicons (apsnd (Scan.extend_lexicon (Symbol.explode name)));
   change_commands (Symtab.update (name, kind));
   Pretty.writeln (report_command (name, kind)));
 
diff -r b52c0c81dcf3 -r 398c64b2acef src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Thu Aug 07 13:44:56 2008 +0200
+++ b/src/Pure/Syntax/syntax.ML	Thu Aug 07 13:45:03 2008 +0200
@@ -296,7 +296,8 @@
   in
     Syntax
     ({input = input',
-      lexicon = if changed then Scan.extend_lexicon (SynExt.delims_of xprods) lexicon else lexicon,
+      lexicon =
+        if changed then fold Scan.extend_lexicon (SynExt.delims_of xprods) lexicon else lexicon,
       gram = if changed then Parser.extend_gram gram xprods else gram,
       consts = Library.merge (op =) (consts1, filter_out NameSpace.is_qualified consts2),
       prmodes = insert (op =) mode (Library.merge (op =) (prmodes1, prmodes2)),
@@ -361,7 +362,7 @@
   in
     Syntax
     ({input = Library.merge (op =) (input1, input2),
-      lexicon = Scan.merge_lexicons lexicon1 lexicon2,
+      lexicon = Scan.merge_lexicons (lexicon1, lexicon2),
       gram = Parser.merge_grams gram1 gram2,
       consts = sort_distinct string_ord (consts1 @ consts2),
       prmodes = Library.merge (op =) (prmodes1, prmodes2),
@@ -464,7 +465,7 @@
   let
     val {lexicon, gram, parse_ast_trtab, ...} = tabs;
     val root' = if root <> "prop" andalso is_logtype root then SynExt.logic else root;
-    val chars = Symbol.explode str;
+    val chars = SymbolPos.explode (str, Position.none);
     val pts = Parser.parse gram root' (Lexicon.tokenize lexicon xids chars);
     val len = length pts;