# HG changeset patch
# User berghofe
# Date 999267472 -7200
# Node ID 9a658fe2010762cfb54bc72ad66ebe317beeb0bf
# Parent  42fbb6abed5afc55515842298c7bc7c2e97411c5
Tuned function extend_lexicon.

diff -r 42fbb6abed5a -r 9a658fe20107 src/Pure/General/scan.ML
--- a/src/Pure/General/scan.ML	Fri Aug 31 16:17:05 2001 +0200
+++ b/src/Pure/General/scan.ML	Fri Aug 31 16:17:52 2001 +0200
@@ -1,6 +1,6 @@
-(*  Title:	Pure/General/scan.ML
-    ID:		$Id$
-    Author:	Markus Wenzel and Tobias Nipkow, TU Muenchen
+(*  Title:      Pure/General/scan.ML
+    ID:         $Id$
+    Author:     Markus Wenzel and Tobias Nipkow, TU Muenchen
     License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Generic scanners (for potentially infinite input).
@@ -76,9 +76,9 @@
 
 (** scanners **)
 
-exception MORE of string option;	(*need more input (prompt)*)
-exception FAIL of string option;	(*try alternatives (reason of failure)*)
-exception ABORT of string;		(*dead end*)
+exception MORE of string option;        (*need more input (prompt)*)
+exception FAIL of string option;        (*try alternatives (reason of failure)*)
+exception ABORT of string;              (*dead end*)
 
 
 (* scanner combinators *)
@@ -129,7 +129,7 @@
 
 fun max leq scan1 scan2 xs =
   (case (option scan1 xs, option scan2 xs) of
-    ((None, _), (None, _)) => raise FAIL None		(*looses FAIL msg!*)
+    ((None, _), (None, _)) => raise FAIL None           (*looses FAIL msg!*)
   | ((Some tok1, xs'), (None, _)) => (tok1, xs')
   | ((None, _), (Some tok2, xs')) => (tok2, xs')
   | ((Some tok1, xs1'), (Some tok2, xs2')) =>
@@ -254,21 +254,22 @@
 
 val empty_lexicon = Empty;
 
-fun extend_lexicon lexicon chrss =
-  let
-    fun ext (lex, chrs) =
+fun extend_lexicon lexicon [] = lexicon
+  | extend_lexicon lexicon chrss =
       let
-	fun add (Branch (d, a, lt, eq, gt)) (chs as c :: cs) =
-	      if c < d then Branch (d, a, add lt chs, eq, gt)
-	      else if c > d then Branch (d, a, lt, eq, add gt chs)
-	      else Branch (d, if null cs then chrs else a, lt, add eq cs, gt)
-	  | add Empty [c] =
-	      Branch (c, chrs, Empty, Empty, Empty)
-	  | add Empty (c :: cs) =
-	      Branch (c, no_literal, Empty, add Empty cs, Empty)
-	  | add lex [] = lex;
-      in add lex chrs end;
-  in foldl ext (lexicon, chrss \\ dest_lex lexicon) end;
+        fun ext (lex, chrs) =
+          let
+            fun add (Branch (d, a, lt, eq, gt)) (chs as c :: cs) =
+                  if c < d then Branch (d, a, add lt chs, eq, gt)
+                  else if c > d then Branch (d, a, lt, eq, add gt chs)
+                  else Branch (d, if null cs then chrs else a, lt, add eq cs, gt)
+              | add Empty [c] =
+                  Branch (c, chrs, Empty, Empty, Empty)
+              | add Empty (c :: cs) =
+                  Branch (c, no_literal, Empty, add Empty cs, Empty)
+              | add lex [] = lex;
+          in add lex chrs end;
+      in foldl ext (lexicon, chrss \\ dest_lex lexicon) end;
 
 val make_lexicon = extend_lexicon empty_lexicon;
 
@@ -290,9 +291,9 @@
     fun lit Empty res _ = res
       | lit (Branch _) _ [] = raise MORE None
       | lit (Branch (d, a, lt, eq, gt)) res (chs as c :: cs) =
-	  if c < d then lit lt res chs
-	  else if c > d then lit gt res chs
-	  else lit eq (if a = no_literal then res else Some (a, cs)) cs;
+          if c < d then lit lt res chs
+          else if c > d then lit gt res chs
+          else lit eq (if a = no_literal then res else Some (a, cs)) cs;
   in
     (case lit lex None chrs of
       None => raise FAIL None