src/Pure/Isar/antiquote.ML
author wenzelm
Wed, 11 Mar 2009 20:54:03 +0100
changeset 30460 c999618d225e
parent 29606 fedb8be05f24
child 30573 49899f26fbd1
permissions -rw-r--r--
debugging: special handling of EXCURSION_FAIL;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
9138
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Isar/antiquote.ML
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
     2
    Author:     Markus Wenzel, TU Muenchen
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
     3
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
     4
Text with antiquotations of inner items (terms, types etc.).
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
     5
*)
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
     6
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
     7
signature ANTIQUOTE =
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
     8
sig
27342
3945da15d410 added Open/Close -- checked blocks;
wenzelm
parents: 26002
diff changeset
     9
  datatype antiquote =
27870
643673ebe065 use SymbolPos.T list directly, instead of encoded SymbolPos.text;
wenzelm
parents: 27835
diff changeset
    10
    Text of string | Antiq of SymbolPos.T list * Position.T |
27342
3945da15d410 added Open/Close -- checked blocks;
wenzelm
parents: 26002
diff changeset
    11
    Open of Position.T | Close of Position.T
9138
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    12
  val is_antiq: antiquote -> bool
27870
643673ebe065 use SymbolPos.T list directly, instead of encoded SymbolPos.text;
wenzelm
parents: 27835
diff changeset
    13
  val read: SymbolPos.T list * Position.T -> antiquote list
27779
4569003b8813 simplified Antiq: regular SymbolPos.text with position;
wenzelm
parents: 27767
diff changeset
    14
  val read_antiq: Scan.lexicon -> (OuterLex.token list -> 'a * OuterLex.token list) ->
27870
643673ebe065 use SymbolPos.T list directly, instead of encoded SymbolPos.text;
wenzelm
parents: 27835
diff changeset
    15
    SymbolPos.T list * Position.T -> 'a
9138
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    16
end;
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    17
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    18
structure Antiquote: ANTIQUOTE =
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    19
struct
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    20
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    21
(* datatype antiquote *)
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    22
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    23
datatype antiquote =
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    24
  Text of string |
27870
643673ebe065 use SymbolPos.T list directly, instead of encoded SymbolPos.text;
wenzelm
parents: 27835
diff changeset
    25
  Antiq of SymbolPos.T list * Position.T |
27342
3945da15d410 added Open/Close -- checked blocks;
wenzelm
parents: 26002
diff changeset
    26
  Open of Position.T |
3945da15d410 added Open/Close -- checked blocks;
wenzelm
parents: 26002
diff changeset
    27
  Close of Position.T;
9138
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    28
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    29
fun is_antiq (Text _) = false
27342
3945da15d410 added Open/Close -- checked blocks;
wenzelm
parents: 26002
diff changeset
    30
  | is_antiq _ = true;
3945da15d410 added Open/Close -- checked blocks;
wenzelm
parents: 26002
diff changeset
    31
3945da15d410 added Open/Close -- checked blocks;
wenzelm
parents: 26002
diff changeset
    32
3945da15d410 added Open/Close -- checked blocks;
wenzelm
parents: 26002
diff changeset
    33
(* check_nesting *)
3945da15d410 added Open/Close -- checked blocks;
wenzelm
parents: 26002
diff changeset
    34
3945da15d410 added Open/Close -- checked blocks;
wenzelm
parents: 26002
diff changeset
    35
fun err_unbalanced pos =
3945da15d410 added Open/Close -- checked blocks;
wenzelm
parents: 26002
diff changeset
    36
  error ("Unbalanced antiquotation block parentheses" ^ Position.str_of pos);
3945da15d410 added Open/Close -- checked blocks;
wenzelm
parents: 26002
diff changeset
    37
3945da15d410 added Open/Close -- checked blocks;
wenzelm
parents: 26002
diff changeset
    38
fun check_nesting antiqs =
3945da15d410 added Open/Close -- checked blocks;
wenzelm
parents: 26002
diff changeset
    39
  let
3945da15d410 added Open/Close -- checked blocks;
wenzelm
parents: 26002
diff changeset
    40
    fun check [] [] = ()
3945da15d410 added Open/Close -- checked blocks;
wenzelm
parents: 26002
diff changeset
    41
      | check [] (pos :: _) = err_unbalanced pos
3945da15d410 added Open/Close -- checked blocks;
wenzelm
parents: 26002
diff changeset
    42
      | check (Open pos :: ants) ps = check ants (pos :: ps)
3945da15d410 added Open/Close -- checked blocks;
wenzelm
parents: 26002
diff changeset
    43
      | check (Close pos :: _) [] = err_unbalanced pos
3945da15d410 added Open/Close -- checked blocks;
wenzelm
parents: 26002
diff changeset
    44
      | check (Close _ :: ants) (_ :: ps) = check ants ps
3945da15d410 added Open/Close -- checked blocks;
wenzelm
parents: 26002
diff changeset
    45
      | check (_ :: ants) ps = check ants ps;
3945da15d410 added Open/Close -- checked blocks;
wenzelm
parents: 26002
diff changeset
    46
  in check antiqs [] end;
9138
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    47
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    48
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    49
(* scan_antiquote *)
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    50
27767
b52c0c81dcf3 renamed scan_antiquotes to read;
wenzelm
parents: 27750
diff changeset
    51
open BasicSymbolPos;
22114
560c5b5dda1c tuned signature;
wenzelm
parents: 19305
diff changeset
    52
structure T = OuterLex;
9138
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    53
22114
560c5b5dda1c tuned signature;
wenzelm
parents: 19305
diff changeset
    54
local
9138
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    55
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    56
val scan_txt =
27767
b52c0c81dcf3 renamed scan_antiquotes to read;
wenzelm
parents: 27750
diff changeset
    57
  $$$ "@" --| Scan.ahead (~$$$ "{") ||
b52c0c81dcf3 renamed scan_antiquotes to read;
wenzelm
parents: 27750
diff changeset
    58
  Scan.one (fn (s, _) => s <> "@" andalso s <> "\\<lbrace>" andalso s <> "\\<rbrace>"
b52c0c81dcf3 renamed scan_antiquotes to read;
wenzelm
parents: 27750
diff changeset
    59
    andalso Symbol.is_regular s) >> single;
9138
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    60
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    61
val scan_ant =
27767
b52c0c81dcf3 renamed scan_antiquotes to read;
wenzelm
parents: 27750
diff changeset
    62
  T.scan_quoted ||
b52c0c81dcf3 renamed scan_antiquotes to read;
wenzelm
parents: 27750
diff changeset
    63
  Scan.one (fn (s, _) => s <> "}" andalso Symbol.is_regular s) >> single;
9138
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    64
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    65
val scan_antiq =
27779
4569003b8813 simplified Antiq: regular SymbolPos.text with position;
wenzelm
parents: 27767
diff changeset
    66
  SymbolPos.scan_pos -- ($$$ "@" |-- $$$ "{" |--
9138
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    67
    T.!!! "missing closing brace of antiquotation"
27779
4569003b8813 simplified Antiq: regular SymbolPos.text with position;
wenzelm
parents: 27767
diff changeset
    68
      (Scan.repeat scan_ant -- ($$$ "}" |-- SymbolPos.scan_pos)))
27870
643673ebe065 use SymbolPos.T list directly, instead of encoded SymbolPos.text;
wenzelm
parents: 27835
diff changeset
    69
  >> (fn (pos1, (body, pos2)) => Antiq (flat body, Position.encode_range (pos1, pos2)));
9138
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    70
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    71
in
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    72
27779
4569003b8813 simplified Antiq: regular SymbolPos.text with position;
wenzelm
parents: 27767
diff changeset
    73
val scan_antiquote =
27799
52f07d5292cd tuned SymbolPos interface;
wenzelm
parents: 27779
diff changeset
    74
 (Scan.repeat1 scan_txt >> (Text o SymbolPos.content o flat) ||
27750
7f5fb39c6362 Antiq: inner vs. outer position;
wenzelm
parents: 27746
diff changeset
    75
  scan_antiq ||
27779
4569003b8813 simplified Antiq: regular SymbolPos.text with position;
wenzelm
parents: 27767
diff changeset
    76
  SymbolPos.scan_pos --| $$$ "\\<lbrace>" >> Open ||
4569003b8813 simplified Antiq: regular SymbolPos.text with position;
wenzelm
parents: 27767
diff changeset
    77
  SymbolPos.scan_pos --| $$$ "\\<rbrace>" >> Close);
9138
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    78
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    79
end;
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    80
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    81
27767
b52c0c81dcf3 renamed scan_antiquotes to read;
wenzelm
parents: 27750
diff changeset
    82
(* read *)
9138
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    83
27880
4ab10bfe8a7f report antiquotations;
wenzelm
parents: 27870
diff changeset
    84
fun report_antiq (Antiq (_, pos)) = Position.report Markup.antiq pos
4ab10bfe8a7f report antiquotations;
wenzelm
parents: 27870
diff changeset
    85
  | report_antiq _ = ();
4ab10bfe8a7f report antiquotations;
wenzelm
parents: 27870
diff changeset
    86
27870
643673ebe065 use SymbolPos.T list directly, instead of encoded SymbolPos.text;
wenzelm
parents: 27835
diff changeset
    87
fun read ([], _) = []
643673ebe065 use SymbolPos.T list directly, instead of encoded SymbolPos.text;
wenzelm
parents: 27835
diff changeset
    88
  | read (syms, pos) =
643673ebe065 use SymbolPos.T list directly, instead of encoded SymbolPos.text;
wenzelm
parents: 27835
diff changeset
    89
      (case Scan.read SymbolPos.stopper (Scan.repeat scan_antiquote) syms of
27880
4ab10bfe8a7f report antiquotations;
wenzelm
parents: 27870
diff changeset
    90
        SOME xs => (List.app report_antiq xs; check_nesting xs; xs)
27767
b52c0c81dcf3 renamed scan_antiquotes to read;
wenzelm
parents: 27750
diff changeset
    91
      | NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos));
9138
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    92
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    93
27779
4569003b8813 simplified Antiq: regular SymbolPos.text with position;
wenzelm
parents: 27767
diff changeset
    94
(* read_antiq *)
22114
560c5b5dda1c tuned signature;
wenzelm
parents: 19305
diff changeset
    95
27870
643673ebe065 use SymbolPos.T list directly, instead of encoded SymbolPos.text;
wenzelm
parents: 27835
diff changeset
    96
fun read_antiq lex scan (syms, pos) =
22114
560c5b5dda1c tuned signature;
wenzelm
parents: 19305
diff changeset
    97
  let
27870
643673ebe065 use SymbolPos.T list directly, instead of encoded SymbolPos.text;
wenzelm
parents: 27835
diff changeset
    98
    fun err msg = cat_error msg ("Malformed antiquotation" ^ Position.str_of pos ^ ":\n" ^
643673ebe065 use SymbolPos.T list directly, instead of encoded SymbolPos.text;
wenzelm
parents: 27835
diff changeset
    99
      "@{" ^ SymbolPos.content syms ^ "}");
22114
560c5b5dda1c tuned signature;
wenzelm
parents: 19305
diff changeset
   100
560c5b5dda1c tuned signature;
wenzelm
parents: 19305
diff changeset
   101
    val res =
27870
643673ebe065 use SymbolPos.T list directly, instead of encoded SymbolPos.text;
wenzelm
parents: 27835
diff changeset
   102
      Source.of_list syms
27835
ff8b8513965a Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents: 27799
diff changeset
   103
      |> T.source' {do_recover = NONE} (K (lex, Scan.empty_lexicon))
22114
560c5b5dda1c tuned signature;
wenzelm
parents: 19305
diff changeset
   104
      |> T.source_proper
27767
b52c0c81dcf3 renamed scan_antiquotes to read;
wenzelm
parents: 27750
diff changeset
   105
      |> Source.source T.stopper (Scan.error (Scan.bulk scan)) NONE
22114
560c5b5dda1c tuned signature;
wenzelm
parents: 19305
diff changeset
   106
      |> Source.exhaust;
560c5b5dda1c tuned signature;
wenzelm
parents: 19305
diff changeset
   107
  in (case res of [x] => x | _ => err "") handle ERROR msg => err msg end;
560c5b5dda1c tuned signature;
wenzelm
parents: 19305
diff changeset
   108
9138
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
   109
end;