src/Pure/General/scan.ML
author paulson
Fri, 05 Oct 2007 09:59:03 +0200
changeset 24854 0ebcd575d3c6
parent 24595 5c290506fbc0
child 25999 f8bcd311d501
permissions -rw-r--r--
filtering out some package theorems
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
11523
9a658fe20107 Tuned function extend_lexicon.
berghofe
parents: 10746
diff changeset
     1
(*  Title:      Pure/General/scan.ML
9a658fe20107 Tuned function extend_lexicon.
berghofe
parents: 10746
diff changeset
     2
    ID:         $Id$
9a658fe20107 Tuned function extend_lexicon.
berghofe
parents: 10746
diff changeset
     3
    Author:     Markus Wenzel and Tobias Nipkow, TU Muenchen
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
     4
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
     5
Generic scanners (for potentially infinite input).
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
     6
*)
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
     7
24025
77e3e5781a99 added :|-- (dependent projection);
wenzelm
parents: 23699
diff changeset
     8
infix 5 -- :-- :|-- |-- --| ^^;
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
     9
infix 3 >>;
23699
5a4527f3ac79 infixr || (more efficient);
wenzelm
parents: 23683
diff changeset
    10
infixr 0 ||;
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    11
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    12
signature BASIC_SCAN =
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    13
sig
14677
33a37f091dc5 tuned presentation;
wenzelm
parents: 14108
diff changeset
    14
  (*error msg handler*)
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    15
  val !! : ('a * string option -> string) -> ('a -> 'b) -> 'a -> 'b
14677
33a37f091dc5 tuned presentation;
wenzelm
parents: 14108
diff changeset
    16
  (*apply function*)
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    17
  val >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c
14677
33a37f091dc5 tuned presentation;
wenzelm
parents: 14108
diff changeset
    18
  (*alternative*)
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    19
  val || : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b
14677
33a37f091dc5 tuned presentation;
wenzelm
parents: 14108
diff changeset
    20
  (*sequential pairing*)
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    21
  val -- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e
14677
33a37f091dc5 tuned presentation;
wenzelm
parents: 14108
diff changeset
    22
  (*dependent pairing*)
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    23
  val :-- : ('a -> 'b * 'c) * ('b -> 'c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e
24025
77e3e5781a99 added :|-- (dependent projection);
wenzelm
parents: 23699
diff changeset
    24
  (*projections*)
77e3e5781a99 added :|-- (dependent projection);
wenzelm
parents: 23699
diff changeset
    25
  val :|-- : ('a -> 'b * 'c) * ('b -> 'c -> 'd * 'e) -> 'a -> 'd * 'e
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    26
  val |-- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'd * 'e
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    27
  val --| : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'b * 'e
14677
33a37f091dc5 tuned presentation;
wenzelm
parents: 14108
diff changeset
    28
  (*concatenation*)
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    29
  val ^^ : ('a -> string * 'b) * ('b -> string * 'c) -> 'a -> string * 'c
14677
33a37f091dc5 tuned presentation;
wenzelm
parents: 14108
diff changeset
    30
  (*one element literal*)
19291
798192b86c41 made $$ and "this" monomorphic (string);
wenzelm
parents: 18683
diff changeset
    31
  val $$ : string -> string list -> string * string list
19306
73137c0b26f5 added ~$$ (negative literal);
wenzelm
parents: 19291
diff changeset
    32
  val ~$$ : string -> string list -> string * string list
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    33
end;
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    34
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    35
signature SCAN =
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    36
sig
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    37
  include BASIC_SCAN
23699
5a4527f3ac79 infixr || (more efficient);
wenzelm
parents: 23683
diff changeset
    38
  val prompt: string -> ('a -> 'b) -> 'a -> 'b
5a4527f3ac79 infixr || (more efficient);
wenzelm
parents: 23683
diff changeset
    39
  val error: ('a -> 'b) -> 'a -> 'b
5a4527f3ac79 infixr || (more efficient);
wenzelm
parents: 23683
diff changeset
    40
  val catch: ('a -> 'b) -> 'a -> 'b    (*exception Fail*)
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    41
  val fail: 'a -> 'b
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    42
  val fail_with: ('a -> string) -> 'a -> 'b
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    43
  val succeed: 'a -> 'b -> 'a * 'b
15664
7c150afba112 added some, peek, trace'; tuned;
wenzelm
parents: 15570
diff changeset
    44
  val some: ('a -> 'b option) -> 'a list -> 'b * 'a list
7c150afba112 added some, peek, trace'; tuned;
wenzelm
parents: 15570
diff changeset
    45
  val one: ('a -> bool) -> 'a list -> 'a * 'a list
19291
798192b86c41 made $$ and "this" monomorphic (string);
wenzelm
parents: 18683
diff changeset
    46
  val this: string list -> string list -> string list * string list
14927
66d797e1b950 added trace (inefficient for very long input);
wenzelm
parents: 14907
diff changeset
    47
  val this_string: string -> string list -> string * string list
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19473
diff changeset
    48
  val many: ('a -> bool) -> 'a list -> 'a list * 'a list
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19473
diff changeset
    49
  val many1: ('a -> bool) -> 'a list -> 'a list * 'a list
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    50
  val optional: ('a -> 'b * 'a) -> 'b -> 'a -> 'b * 'a
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    51
  val option: ('a -> 'b * 'a) -> 'a -> 'b option * 'a
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    52
  val repeat: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    53
  val repeat1: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
23699
5a4527f3ac79 infixr || (more efficient);
wenzelm
parents: 23683
diff changeset
    54
  val single: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
5a4527f3ac79 infixr || (more efficient);
wenzelm
parents: 23683
diff changeset
    55
  val bulk: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    56
  val max: ('a * 'a -> bool) -> ('b -> 'a * 'b) -> ('b -> 'a * 'b) -> 'b -> 'a * 'b
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    57
  val ahead: ('a -> 'b * 'c) -> 'a -> 'b * 'a
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    58
  val unless: ('a -> 'b * 'a) -> ('a -> 'c * 'd) -> 'a -> 'c * 'd
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    59
  val first: ('a -> 'b) list -> 'a -> 'b
14677
33a37f091dc5 tuned presentation;
wenzelm
parents: 14108
diff changeset
    60
  val state: 'a * 'b -> 'a * ('a * 'b)
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    61
  val depend: ('a -> 'b -> ('c * 'd) * 'e) -> 'a * 'b -> 'd * ('c * 'e)
15664
7c150afba112 added some, peek, trace'; tuned;
wenzelm
parents: 15570
diff changeset
    62
  val peek: ('a -> 'b -> 'c * 'd) -> 'a * 'b -> 'c * ('a * 'd)
7c150afba112 added some, peek, trace'; tuned;
wenzelm
parents: 15570
diff changeset
    63
  val pass: 'a -> ('a * 'b -> 'c * ('d * 'e)) -> 'b -> 'c * 'e
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    64
  val lift: ('a -> 'b * 'c) -> 'd * 'a -> 'b * ('d * 'c)
23699
5a4527f3ac79 infixr || (more efficient);
wenzelm
parents: 23683
diff changeset
    65
  val unlift: (unit * 'a -> 'b * ('c * 'd)) -> 'a -> 'b * 'd
15664
7c150afba112 added some, peek, trace'; tuned;
wenzelm
parents: 15570
diff changeset
    66
  val trace: ('a list -> 'b * 'c list) -> 'a list -> ('b * 'a list) * 'c list
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    67
  val finite': 'a * ('a -> bool) -> ('b * 'a list -> 'c * ('d * 'a list))
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    68
    -> 'b * 'a list -> 'c * ('d * 'a list)
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    69
  val finite: 'a * ('a -> bool) -> ('a list -> 'b * 'a list) -> 'a list -> 'b * 'a list
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    70
  val read: 'a * ('a -> bool) -> ('a list -> 'b * 'a list) -> 'a list -> 'b option
23699
5a4527f3ac79 infixr || (more efficient);
wenzelm
parents: 23683
diff changeset
    71
  val drain: string -> (string -> 'a -> 'b list * 'a) -> 'b * ('b -> bool) ->
5a4527f3ac79 infixr || (more efficient);
wenzelm
parents: 23683
diff changeset
    72
    ('c * 'b list -> 'd * ('e * 'b list)) -> ('c * 'b list) * 'a -> ('d * ('e * 'b list)) * 'a
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    73
  type lexicon
7025
afbd8241797b tuned dest_lexicon;
wenzelm
parents: 6640
diff changeset
    74
  val dest_lexicon: lexicon -> string list
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    75
  val make_lexicon: string list list -> lexicon
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    76
  val empty_lexicon: lexicon
22112
6a90ac654c6d tuned signature of extend_lexicon;
wenzelm
parents: 21858
diff changeset
    77
  val extend_lexicon: string list list -> lexicon -> lexicon
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    78
  val merge_lexicons: lexicon -> lexicon -> lexicon
14686
708c613370ab added is_literal;
wenzelm
parents: 14677
diff changeset
    79
  val is_literal: lexicon -> string list -> bool
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    80
  val literal: lexicon -> string list -> string list * string list
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    81
end;
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    82
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    83
structure Scan: SCAN =
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    84
struct
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    85
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    86
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    87
(** scanners **)
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    88
23699
5a4527f3ac79 infixr || (more efficient);
wenzelm
parents: 23683
diff changeset
    89
(* exceptions *)
5a4527f3ac79 infixr || (more efficient);
wenzelm
parents: 23683
diff changeset
    90
11523
9a658fe20107 Tuned function extend_lexicon.
berghofe
parents: 10746
diff changeset
    91
exception MORE of string option;        (*need more input (prompt)*)
9a658fe20107 Tuned function extend_lexicon.
berghofe
parents: 10746
diff changeset
    92
exception FAIL of string option;        (*try alternatives (reason of failure)*)
9a658fe20107 Tuned function extend_lexicon.
berghofe
parents: 10746
diff changeset
    93
exception ABORT of string;              (*dead end*)
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    94
23699
5a4527f3ac79 infixr || (more efficient);
wenzelm
parents: 23683
diff changeset
    95
fun !! err scan xs = scan xs handle FAIL msg => raise ABORT (err (xs, msg));
5a4527f3ac79 infixr || (more efficient);
wenzelm
parents: 23683
diff changeset
    96
fun permissive scan xs = scan xs handle MORE _ => raise FAIL NONE | ABORT _ => raise FAIL NONE;
5a4527f3ac79 infixr || (more efficient);
wenzelm
parents: 23683
diff changeset
    97
fun strict scan xs = scan xs handle MORE _ => raise FAIL NONE;
5a4527f3ac79 infixr || (more efficient);
wenzelm
parents: 23683
diff changeset
    98
fun prompt str scan xs = scan xs handle MORE NONE => raise MORE (SOME str);
5a4527f3ac79 infixr || (more efficient);
wenzelm
parents: 23683
diff changeset
    99
fun error scan xs = scan xs handle ABORT msg => Library.error msg;
5a4527f3ac79 infixr || (more efficient);
wenzelm
parents: 23683
diff changeset
   100
5a4527f3ac79 infixr || (more efficient);
wenzelm
parents: 23683
diff changeset
   101
fun catch scan xs = scan xs
5a4527f3ac79 infixr || (more efficient);
wenzelm
parents: 23683
diff changeset
   102
  handle ABORT msg => raise Fail msg
5a4527f3ac79 infixr || (more efficient);
wenzelm
parents: 23683
diff changeset
   103
    | FAIL msg => raise Fail (the_default "Syntax error." msg);
5a4527f3ac79 infixr || (more efficient);
wenzelm
parents: 23683
diff changeset
   104
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   105
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   106
(* scanner combinators *)
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   107
19306
73137c0b26f5 added ~$$ (negative literal);
wenzelm
parents: 19291
diff changeset
   108
fun (scan >> f) xs = scan xs |>> f;
14078
cddad2aa025b integrated optimizations by Sebastian Skalberg,
kleing
parents: 13795
diff changeset
   109
19306
73137c0b26f5 added ~$$ (negative literal);
wenzelm
parents: 19291
diff changeset
   110
fun (scan1 || scan2) xs = scan1 xs handle FAIL _ => scan2 xs;
14078
cddad2aa025b integrated optimizations by Sebastian Skalberg,
kleing
parents: 13795
diff changeset
   111
19306
73137c0b26f5 added ~$$ (negative literal);
wenzelm
parents: 19291
diff changeset
   112
fun (scan1 :-- scan2) xs =
14108
eaf3c75f2c8e Restored old (tail recursive!) version of repeat.
berghofe
parents: 14078
diff changeset
   113
  let
19306
73137c0b26f5 added ~$$ (negative literal);
wenzelm
parents: 19291
diff changeset
   114
    val (x, ys) = scan1 xs;
73137c0b26f5 added ~$$ (negative literal);
wenzelm
parents: 19291
diff changeset
   115
    val (y, zs) = scan2 x ys;
73137c0b26f5 added ~$$ (negative literal);
wenzelm
parents: 19291
diff changeset
   116
  in ((x, y), zs) end;
14078
cddad2aa025b integrated optimizations by Sebastian Skalberg,
kleing
parents: 13795
diff changeset
   117
19306
73137c0b26f5 added ~$$ (negative literal);
wenzelm
parents: 19291
diff changeset
   118
fun (scan1 -- scan2) = scan1 :-- (fn _ => scan2);
24025
77e3e5781a99 added :|-- (dependent projection);
wenzelm
parents: 23699
diff changeset
   119
fun (scan1 :|-- scan2) = scan1 :-- scan2 >> #2;
19306
73137c0b26f5 added ~$$ (negative literal);
wenzelm
parents: 19291
diff changeset
   120
fun (scan1 |-- scan2) = scan1 -- scan2 >> #2;
73137c0b26f5 added ~$$ (negative literal);
wenzelm
parents: 19291
diff changeset
   121
fun (scan1 --| scan2) = scan1 -- scan2 >> #1;
73137c0b26f5 added ~$$ (negative literal);
wenzelm
parents: 19291
diff changeset
   122
fun (scan1 ^^ scan2) = scan1 -- scan2 >> op ^;
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   123
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   124
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   125
(* generic scanners *)
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   126
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   127
fun fail _ = raise FAIL NONE;
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   128
fun fail_with msg_of xs = raise FAIL (SOME (msg_of xs));
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   129
fun succeed y xs = (y, xs);
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   130
15664
7c150afba112 added some, peek, trace'; tuned;
wenzelm
parents: 15570
diff changeset
   131
fun some _ [] = raise MORE NONE
7c150afba112 added some, peek, trace'; tuned;
wenzelm
parents: 15570
diff changeset
   132
  | some f (x :: xs) =
7c150afba112 added some, peek, trace'; tuned;
wenzelm
parents: 15570
diff changeset
   133
      (case f x of SOME y => (y, xs) | _ => raise FAIL NONE);
7c150afba112 added some, peek, trace'; tuned;
wenzelm
parents: 15570
diff changeset
   134
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   135
fun one _ [] = raise MORE NONE
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   136
  | one pred (x :: xs) =
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   137
      if pred x then (x, xs) else raise FAIL NONE;
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   138
19306
73137c0b26f5 added ~$$ (negative literal);
wenzelm
parents: 19291
diff changeset
   139
fun $$ a = one (fn s: string => s = a);
73137c0b26f5 added ~$$ (negative literal);
wenzelm
parents: 19291
diff changeset
   140
fun ~$$ a = one (fn s: string => s <> a);
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   141
14833
30556b84af7c Output.error;
wenzelm
parents: 14726
diff changeset
   142
fun this ys xs =
14726
9657c23cc3e7 added Scan.list;
wenzelm
parents: 14686
diff changeset
   143
  let
9657c23cc3e7 added Scan.list;
wenzelm
parents: 14686
diff changeset
   144
    fun drop_prefix [] xs = xs
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   145
      | drop_prefix (_ :: _) [] = raise MORE NONE
14726
9657c23cc3e7 added Scan.list;
wenzelm
parents: 14686
diff changeset
   146
      | drop_prefix (y :: ys) (x :: xs) =
19291
798192b86c41 made $$ and "this" monomorphic (string);
wenzelm
parents: 18683
diff changeset
   147
          if (y: string) = x then drop_prefix ys xs else raise FAIL NONE;
14726
9657c23cc3e7 added Scan.list;
wenzelm
parents: 14686
diff changeset
   148
  in (ys, drop_prefix ys xs) end;
9657c23cc3e7 added Scan.list;
wenzelm
parents: 14686
diff changeset
   149
15664
7c150afba112 added some, peek, trace'; tuned;
wenzelm
parents: 15570
diff changeset
   150
fun this_string s = this (explode s) >> K s;  (*primitive string -- no symbols here!*)
14907
c77fda9b6cf0 added this_string;
wenzelm
parents: 14833
diff changeset
   151
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19473
diff changeset
   152
fun many _ [] = raise MORE NONE
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19473
diff changeset
   153
  | many pred (lst as x :: xs) =
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19473
diff changeset
   154
      if pred x then apfst (cons x) (many pred xs)
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   155
      else ([], lst);
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   156
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19473
diff changeset
   157
fun many1 pred = one pred -- many pred >> op ::;
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   158
15664
7c150afba112 added some, peek, trace'; tuned;
wenzelm
parents: 15570
diff changeset
   159
fun optional scan def = scan || succeed def;
7c150afba112 added some, peek, trace'; tuned;
wenzelm
parents: 15570
diff changeset
   160
fun option scan = (scan >> SOME) || succeed NONE;
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   161
13795
cfa3441c5238 Some tuning:
berghofe
parents: 11523
diff changeset
   162
fun repeat scan =
15664
7c150afba112 added some, peek, trace'; tuned;
wenzelm
parents: 15570
diff changeset
   163
  let
7c150afba112 added some, peek, trace'; tuned;
wenzelm
parents: 15570
diff changeset
   164
    fun rep ys xs =
7c150afba112 added some, peek, trace'; tuned;
wenzelm
parents: 15570
diff changeset
   165
      (case (SOME (scan xs) handle FAIL _ => NONE) of
7c150afba112 added some, peek, trace'; tuned;
wenzelm
parents: 15570
diff changeset
   166
        NONE => (rev ys, xs)
7c150afba112 added some, peek, trace'; tuned;
wenzelm
parents: 15570
diff changeset
   167
      | SOME (y, xs') => rep (y :: ys) xs');
14108
eaf3c75f2c8e Restored old (tail recursive!) version of repeat.
berghofe
parents: 14078
diff changeset
   168
  in rep [] end;
13795
cfa3441c5238 Some tuning:
berghofe
parents: 11523
diff changeset
   169
15664
7c150afba112 added some, peek, trace'; tuned;
wenzelm
parents: 15570
diff changeset
   170
fun repeat1 scan = scan -- repeat scan >> op ::;
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   171
23699
5a4527f3ac79 infixr || (more efficient);
wenzelm
parents: 23683
diff changeset
   172
fun single scan = scan >> (fn x => [x]);
5a4527f3ac79 infixr || (more efficient);
wenzelm
parents: 23683
diff changeset
   173
fun bulk scan = scan -- repeat (permissive scan) >> (op ::);
5a4527f3ac79 infixr || (more efficient);
wenzelm
parents: 23683
diff changeset
   174
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   175
fun max leq scan1 scan2 xs =
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   176
  (case (option scan1 xs, option scan2 xs) of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   177
    ((NONE, _), (NONE, _)) => raise FAIL NONE           (*looses FAIL msg!*)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   178
  | ((SOME tok1, xs'), (NONE, _)) => (tok1, xs')
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   179
  | ((NONE, _), (SOME tok2, xs')) => (tok2, xs')
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   180
  | ((SOME tok1, xs1'), (SOME tok2, xs2')) =>
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   181
      if leq (tok2, tok1) then (tok1, xs1') else (tok2, xs2'));
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   182
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   183
fun ahead scan xs = (fst (scan xs), xs);
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   184
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   185
fun unless test scan =
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   186
  ahead (option test) :-- (fn NONE => scan | _ => fail) >> #2;
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   187
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   188
fun first [] = fail
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   189
  | first (scan :: scans) = scan || first scans;
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   190
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   191
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   192
(* state based scanners *)
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   193
9122
addbea344673 added state: 'a * 'b -> 'a * ('a * 'b);
wenzelm
parents: 8806
diff changeset
   194
fun state (st, xs) = (st, (st, xs));
addbea344673 added state: 'a * 'b -> 'a * ('a * 'b);
wenzelm
parents: 8806
diff changeset
   195
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   196
fun depend scan (st, xs) =
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   197
  let val ((st', y), xs') = scan st xs
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   198
  in (y, (st', xs')) end;
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   199
15664
7c150afba112 added some, peek, trace'; tuned;
wenzelm
parents: 15570
diff changeset
   200
fun peek scan = depend (fn st => scan st >> pair st);
7c150afba112 added some, peek, trace'; tuned;
wenzelm
parents: 15570
diff changeset
   201
7c150afba112 added some, peek, trace'; tuned;
wenzelm
parents: 15570
diff changeset
   202
fun pass st scan xs =
7c150afba112 added some, peek, trace'; tuned;
wenzelm
parents: 15570
diff changeset
   203
  let val (y, (_, xs')) = scan (st, xs)
7c150afba112 added some, peek, trace'; tuned;
wenzelm
parents: 15570
diff changeset
   204
  in (y, xs') end;
7c150afba112 added some, peek, trace'; tuned;
wenzelm
parents: 15570
diff changeset
   205
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   206
fun lift scan (st, xs) =
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   207
  let val (y, xs') = scan xs
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   208
  in (y, (st, xs')) end;
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   209
15664
7c150afba112 added some, peek, trace'; tuned;
wenzelm
parents: 15570
diff changeset
   210
fun unlift scan = pass () scan;
7c150afba112 added some, peek, trace'; tuned;
wenzelm
parents: 15570
diff changeset
   211
7c150afba112 added some, peek, trace'; tuned;
wenzelm
parents: 15570
diff changeset
   212
7c150afba112 added some, peek, trace'; tuned;
wenzelm
parents: 15570
diff changeset
   213
(* trace input *)
7c150afba112 added some, peek, trace'; tuned;
wenzelm
parents: 15570
diff changeset
   214
23699
5a4527f3ac79 infixr || (more efficient);
wenzelm
parents: 23683
diff changeset
   215
fun trace scan xs =
5a4527f3ac79 infixr || (more efficient);
wenzelm
parents: 23683
diff changeset
   216
  let val (y, xs') = scan xs
5a4527f3ac79 infixr || (more efficient);
wenzelm
parents: 23683
diff changeset
   217
  in ((y, Library.take (length xs - length xs', xs)), xs') end;
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   218
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   219
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   220
(* finite scans *)
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   221
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   222
fun finite' (stopper, is_stopper) scan (state, input) =
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   223
  let
24595
5c290506fbc0 tuned message;
wenzelm
parents: 24025
diff changeset
   224
    fun lost () = raise ABORT "Bad scanner: lost stopper of finite scan!";
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   225
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   226
    fun stop [] = lost ()
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   227
      | stop lst =
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   228
          let val (xs, x) = split_last lst
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   229
          in if is_stopper x then ((), xs) else lost () end;
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   230
  in
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   231
    if exists is_stopper input then
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   232
      raise ABORT "Stopper may not occur in input of finite scan!"
23674
c7cbab93f1d9 tuned signature;
wenzelm
parents: 22112
diff changeset
   233
    else (strict scan --| lift stop) (state, input @ [stopper])
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   234
  end;
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   235
15664
7c150afba112 added some, peek, trace'; tuned;
wenzelm
parents: 15570
diff changeset
   236
fun finite stopper scan = unlift (finite' stopper (lift scan));
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   237
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   238
fun read stopper scan xs =
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   239
  (case error (finite stopper (option scan)) xs of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   240
    (y as SOME _, []) => y
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   241
  | _ => NONE);
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   242
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   243
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   244
(* infinite scans -- draining state-based source *)
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   245
23699
5a4527f3ac79 infixr || (more efficient);
wenzelm
parents: 23683
diff changeset
   246
fun drain def_prompt get stopper scan ((state, xs), src) =
5a4527f3ac79 infixr || (more efficient);
wenzelm
parents: 23683
diff changeset
   247
  (scan (state, xs), src) handle MORE prompt =>
5a4527f3ac79 infixr || (more efficient);
wenzelm
parents: 23683
diff changeset
   248
    (case get (the_default def_prompt prompt) src of
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   249
      ([], _) => (finite' stopper scan (state, xs), src)
23699
5a4527f3ac79 infixr || (more efficient);
wenzelm
parents: 23683
diff changeset
   250
    | (xs', src') => drain def_prompt get stopper scan ((state, xs @ xs'), src'));
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   251
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   252
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   253
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   254
(** datatype lexicon **)
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   255
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   256
datatype lexicon =
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   257
  Empty |
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   258
  Branch of string * string list * lexicon * lexicon * lexicon;
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   259
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   260
val no_literal = [];
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   261
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   262
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   263
(* dest_lexicon *)
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   264
7025
afbd8241797b tuned dest_lexicon;
wenzelm
parents: 6640
diff changeset
   265
fun dest_lex Empty = []
afbd8241797b tuned dest_lexicon;
wenzelm
parents: 6640
diff changeset
   266
  | dest_lex (Branch (_, [], lt, eq, gt)) =
afbd8241797b tuned dest_lexicon;
wenzelm
parents: 6640
diff changeset
   267
      dest_lex lt @ dest_lex eq @ dest_lex gt
afbd8241797b tuned dest_lexicon;
wenzelm
parents: 6640
diff changeset
   268
  | dest_lex (Branch (_, cs, lt, eq, gt)) =
afbd8241797b tuned dest_lexicon;
wenzelm
parents: 6640
diff changeset
   269
      dest_lex lt @ [cs] @ dest_lex eq @ dest_lex gt;
afbd8241797b tuned dest_lexicon;
wenzelm
parents: 6640
diff changeset
   270
afbd8241797b tuned dest_lexicon;
wenzelm
parents: 6640
diff changeset
   271
val dest_lexicon = map implode o dest_lex;
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   272
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   273
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   274
(* empty, extend, make, merge lexicons *)
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   275
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   276
val empty_lexicon = Empty;
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   277
22112
6a90ac654c6d tuned signature of extend_lexicon;
wenzelm
parents: 21858
diff changeset
   278
fun extend_lexicon [] lexicon = lexicon
6a90ac654c6d tuned signature of extend_lexicon;
wenzelm
parents: 21858
diff changeset
   279
  | extend_lexicon chrss lexicon =
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   280
      let
19306
73137c0b26f5 added ~$$ (negative literal);
wenzelm
parents: 19291
diff changeset
   281
        fun ext chrs lex =
11523
9a658fe20107 Tuned function extend_lexicon.
berghofe
parents: 10746
diff changeset
   282
          let
19306
73137c0b26f5 added ~$$ (negative literal);
wenzelm
parents: 19291
diff changeset
   283
            fun add (chs as c :: cs) (Branch (d, a, lt, eq, gt)) =
73137c0b26f5 added ~$$ (negative literal);
wenzelm
parents: 19291
diff changeset
   284
                  (case fast_string_ord (c, d) of
73137c0b26f5 added ~$$ (negative literal);
wenzelm
parents: 19291
diff changeset
   285
                    LESS => Branch (d, a, add chs lt, eq, gt)
73137c0b26f5 added ~$$ (negative literal);
wenzelm
parents: 19291
diff changeset
   286
                  | EQUAL => Branch (d, if null cs then chrs else a, lt, add cs eq, gt)
73137c0b26f5 added ~$$ (negative literal);
wenzelm
parents: 19291
diff changeset
   287
                  | GREATER => Branch (d, a, lt, eq, add chs gt))
73137c0b26f5 added ~$$ (negative literal);
wenzelm
parents: 19291
diff changeset
   288
              | add [c] Empty = Branch (c, chrs, Empty, Empty, Empty)
73137c0b26f5 added ~$$ (negative literal);
wenzelm
parents: 19291
diff changeset
   289
              | add (c :: cs) Empty = Branch (c, no_literal, Empty, add cs Empty, Empty)
73137c0b26f5 added ~$$ (negative literal);
wenzelm
parents: 19291
diff changeset
   290
              | add [] lex = lex;
73137c0b26f5 added ~$$ (negative literal);
wenzelm
parents: 19291
diff changeset
   291
          in add chrs lex end;
73137c0b26f5 added ~$$ (negative literal);
wenzelm
parents: 19291
diff changeset
   292
      in lexicon |> fold ext (chrss |> subtract (op =) (dest_lex lexicon)) end;
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   293
22112
6a90ac654c6d tuned signature of extend_lexicon;
wenzelm
parents: 21858
diff changeset
   294
fun make_lexicon chrss = extend_lexicon chrss empty_lexicon;
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   295
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   296
fun merge_lexicons lex1 lex2 =
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   297
  let
7025
afbd8241797b tuned dest_lexicon;
wenzelm
parents: 6640
diff changeset
   298
    val chss1 = dest_lex lex1;
afbd8241797b tuned dest_lexicon;
wenzelm
parents: 6640
diff changeset
   299
    val chss2 = dest_lex lex2;
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   300
  in
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   301
    if chss2 subset chss1 then lex1
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   302
    else if chss1 subset chss2 then lex2
22112
6a90ac654c6d tuned signature of extend_lexicon;
wenzelm
parents: 21858
diff changeset
   303
    else extend_lexicon chss2 lex1
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   304
  end;
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   305
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   306
14686
708c613370ab added is_literal;
wenzelm
parents: 14677
diff changeset
   307
(* is_literal *)
708c613370ab added is_literal;
wenzelm
parents: 14677
diff changeset
   308
708c613370ab added is_literal;
wenzelm
parents: 14677
diff changeset
   309
fun is_literal Empty _ = false
708c613370ab added is_literal;
wenzelm
parents: 14677
diff changeset
   310
  | is_literal _ [] = false
708c613370ab added is_literal;
wenzelm
parents: 14677
diff changeset
   311
  | is_literal (Branch (d, a, lt, eq, gt)) (chs as c :: cs) =
19306
73137c0b26f5 added ~$$ (negative literal);
wenzelm
parents: 19291
diff changeset
   312
      (case fast_string_ord (c, d) of
14686
708c613370ab added is_literal;
wenzelm
parents: 14677
diff changeset
   313
        LESS => is_literal lt chs
708c613370ab added is_literal;
wenzelm
parents: 14677
diff changeset
   314
      | EQUAL => a <> no_literal andalso null cs orelse is_literal eq cs
708c613370ab added is_literal;
wenzelm
parents: 14677
diff changeset
   315
      | GREATER => is_literal gt chs);
708c613370ab added is_literal;
wenzelm
parents: 14677
diff changeset
   316
708c613370ab added is_literal;
wenzelm
parents: 14677
diff changeset
   317
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   318
(* scan literal *)
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   319
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   320
fun literal lex chrs =
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   321
  let
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   322
    fun lit Empty res _ = res
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   323
      | lit (Branch _) _ [] = raise MORE NONE
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   324
      | lit (Branch (d, a, lt, eq, gt)) res (chs as c :: cs) =
19306
73137c0b26f5 added ~$$ (negative literal);
wenzelm
parents: 19291
diff changeset
   325
          (case fast_string_ord (c, d) of
14686
708c613370ab added is_literal;
wenzelm
parents: 14677
diff changeset
   326
            LESS => lit lt res chs
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   327
          | EQUAL => lit eq (if a = no_literal then res else SOME (a, cs)) cs
14686
708c613370ab added is_literal;
wenzelm
parents: 14677
diff changeset
   328
          | GREATER => lit gt res chs);
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   329
  in
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   330
    (case lit lex NONE chrs of
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   331
      NONE => raise FAIL NONE
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   332
    | SOME res => res)
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   333
  end;
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   334
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   335
end;
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   336
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   337
structure BasicScan: BASIC_SCAN = Scan;
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   338
open BasicScan;