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