src/Pure/General/antiquote.ML
author wenzelm
Fri, 20 Mar 2009 20:21:38 +0100
changeset 30613 b22d35d9ef28
parent 30590 1d9c9fcf8513
child 30635 a7d175c48228
permissions -rw-r--r--
Antiquote.read: argument for reporting text;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
30587
ad19c99529eb moved Isar/antiquote.ML to General/antiquote.ML, which is loaded early;
wenzelm
parents: 30573
diff changeset
     1
(*  Title:      Pure/General/antiquote.ML
9138
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
30587
ad19c99529eb moved Isar/antiquote.ML to General/antiquote.ML, which is loaded early;
wenzelm
parents: 30573
diff changeset
     4
Text with antiquotations of inner items (types, terms, theorems etc.).
9138
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
30590
1d9c9fcf8513 parameterized datatype antiquote and read operation;
wenzelm
parents: 30589
diff changeset
     9
  datatype 'a antiquote =
1d9c9fcf8513 parameterized datatype antiquote and read operation;
wenzelm
parents: 30589
diff changeset
    10
    Text of 'a |
1d9c9fcf8513 parameterized datatype antiquote and read operation;
wenzelm
parents: 30589
diff changeset
    11
    Antiq of Symbol_Pos.T list * Position.T |
1d9c9fcf8513 parameterized datatype antiquote and read operation;
wenzelm
parents: 30589
diff changeset
    12
    Open of Position.T |
1d9c9fcf8513 parameterized datatype antiquote and read operation;
wenzelm
parents: 30589
diff changeset
    13
    Close of Position.T
1d9c9fcf8513 parameterized datatype antiquote and read operation;
wenzelm
parents: 30589
diff changeset
    14
  val is_antiq: 'a antiquote -> bool
1d9c9fcf8513 parameterized datatype antiquote and read operation;
wenzelm
parents: 30589
diff changeset
    15
  val scan: Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list
1d9c9fcf8513 parameterized datatype antiquote and read operation;
wenzelm
parents: 30589
diff changeset
    16
  val scan_text: Symbol_Pos.T list -> Symbol_Pos.T list antiquote * Symbol_Pos.T list
30613
b22d35d9ef28 Antiquote.read: argument for reporting text;
wenzelm
parents: 30590
diff changeset
    17
  val read: ('a -> unit) -> (Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list) ->
30590
1d9c9fcf8513 parameterized datatype antiquote and read operation;
wenzelm
parents: 30589
diff changeset
    18
    Symbol_Pos.T list * Position.T -> 'a antiquote list
9138
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    19
end;
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
structure Antiquote: ANTIQUOTE =
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    22
struct
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    23
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    24
(* datatype antiquote *)
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    25
30590
1d9c9fcf8513 parameterized datatype antiquote and read operation;
wenzelm
parents: 30589
diff changeset
    26
datatype 'a antiquote =
1d9c9fcf8513 parameterized datatype antiquote and read operation;
wenzelm
parents: 30589
diff changeset
    27
  Text of 'a |
30573
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 29606
diff changeset
    28
  Antiq of Symbol_Pos.T list * Position.T |
27342
3945da15d410 added Open/Close -- checked blocks;
wenzelm
parents: 26002
diff changeset
    29
  Open of Position.T |
3945da15d410 added Open/Close -- checked blocks;
wenzelm
parents: 26002
diff changeset
    30
  Close of Position.T;
9138
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    31
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    32
fun is_antiq (Text _) = false
27342
3945da15d410 added Open/Close -- checked blocks;
wenzelm
parents: 26002
diff changeset
    33
  | is_antiq _ = true;
3945da15d410 added Open/Close -- checked blocks;
wenzelm
parents: 26002
diff changeset
    34
3945da15d410 added Open/Close -- checked blocks;
wenzelm
parents: 26002
diff changeset
    35
3945da15d410 added Open/Close -- checked blocks;
wenzelm
parents: 26002
diff changeset
    36
(* check_nesting *)
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 err_unbalanced pos =
3945da15d410 added Open/Close -- checked blocks;
wenzelm
parents: 26002
diff changeset
    39
  error ("Unbalanced antiquotation block parentheses" ^ Position.str_of pos);
3945da15d410 added Open/Close -- checked blocks;
wenzelm
parents: 26002
diff changeset
    40
3945da15d410 added Open/Close -- checked blocks;
wenzelm
parents: 26002
diff changeset
    41
fun check_nesting antiqs =
3945da15d410 added Open/Close -- checked blocks;
wenzelm
parents: 26002
diff changeset
    42
  let
3945da15d410 added Open/Close -- checked blocks;
wenzelm
parents: 26002
diff changeset
    43
    fun check [] [] = ()
3945da15d410 added Open/Close -- checked blocks;
wenzelm
parents: 26002
diff changeset
    44
      | check [] (pos :: _) = err_unbalanced pos
3945da15d410 added Open/Close -- checked blocks;
wenzelm
parents: 26002
diff changeset
    45
      | check (Open pos :: ants) ps = check ants (pos :: ps)
3945da15d410 added Open/Close -- checked blocks;
wenzelm
parents: 26002
diff changeset
    46
      | check (Close pos :: _) [] = err_unbalanced pos
3945da15d410 added Open/Close -- checked blocks;
wenzelm
parents: 26002
diff changeset
    47
      | check (Close _ :: ants) (_ :: ps) = check ants ps
3945da15d410 added Open/Close -- checked blocks;
wenzelm
parents: 26002
diff changeset
    48
      | check (_ :: ants) ps = check ants ps;
3945da15d410 added Open/Close -- checked blocks;
wenzelm
parents: 26002
diff changeset
    49
  in check antiqs [] end;
9138
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    50
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    51
30590
1d9c9fcf8513 parameterized datatype antiquote and read operation;
wenzelm
parents: 30589
diff changeset
    52
(* scan *)
9138
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    53
30573
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 29606
diff changeset
    54
open Basic_Symbol_Pos;
9138
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    55
22114
560c5b5dda1c tuned signature;
wenzelm
parents: 19305
diff changeset
    56
local
9138
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    57
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    58
val scan_txt =
27767
b52c0c81dcf3 renamed scan_antiquotes to read;
wenzelm
parents: 27750
diff changeset
    59
  $$$ "@" --| Scan.ahead (~$$$ "{") ||
b52c0c81dcf3 renamed scan_antiquotes to read;
wenzelm
parents: 27750
diff changeset
    60
  Scan.one (fn (s, _) => s <> "@" andalso s <> "\\<lbrace>" andalso s <> "\\<rbrace>"
b52c0c81dcf3 renamed scan_antiquotes to read;
wenzelm
parents: 27750
diff changeset
    61
    andalso Symbol.is_regular s) >> single;
9138
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    62
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    63
val scan_ant =
30587
ad19c99529eb moved Isar/antiquote.ML to General/antiquote.ML, which is loaded early;
wenzelm
parents: 30573
diff changeset
    64
  Symbol_Pos.scan_quoted ||
27767
b52c0c81dcf3 renamed scan_antiquotes to read;
wenzelm
parents: 27750
diff changeset
    65
  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
    66
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    67
val scan_antiq =
30573
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 29606
diff changeset
    68
  Symbol_Pos.scan_pos -- ($$$ "@" |-- $$$ "{" |--
30587
ad19c99529eb moved Isar/antiquote.ML to General/antiquote.ML, which is loaded early;
wenzelm
parents: 30573
diff changeset
    69
    Symbol_Pos.!!! "missing closing brace of antiquotation"
30573
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 29606
diff changeset
    70
      (Scan.repeat scan_ant -- ($$$ "}" |-- Symbol_Pos.scan_pos)))
30590
1d9c9fcf8513 parameterized datatype antiquote and read operation;
wenzelm
parents: 30589
diff changeset
    71
  >> (fn (pos1, (body, pos2)) => (flat body, Position.encode_range (pos1, pos2)));
1d9c9fcf8513 parameterized datatype antiquote and read operation;
wenzelm
parents: 30589
diff changeset
    72
1d9c9fcf8513 parameterized datatype antiquote and read operation;
wenzelm
parents: 30589
diff changeset
    73
val scan_open = Symbol_Pos.scan_pos --| $$$ "\\<lbrace>";
1d9c9fcf8513 parameterized datatype antiquote and read operation;
wenzelm
parents: 30589
diff changeset
    74
val scan_close = Symbol_Pos.scan_pos --| $$$ "\\<rbrace>";
9138
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    75
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    76
in
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    77
30590
1d9c9fcf8513 parameterized datatype antiquote and read operation;
wenzelm
parents: 30589
diff changeset
    78
fun scan x = (scan_antiq >> Antiq || scan_open >> Open || scan_close >> Close) x;
1d9c9fcf8513 parameterized datatype antiquote and read operation;
wenzelm
parents: 30589
diff changeset
    79
val scan_text = scan || Scan.repeat1 scan_txt >> (Text o flat);
9138
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
end;
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    82
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    83
27767
b52c0c81dcf3 renamed scan_antiquotes to read;
wenzelm
parents: 27750
diff changeset
    84
(* read *)
9138
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    85
30613
b22d35d9ef28 Antiquote.read: argument for reporting text;
wenzelm
parents: 30590
diff changeset
    86
fun read _ _ ([], _) = []
b22d35d9ef28 Antiquote.read: argument for reporting text;
wenzelm
parents: 30590
diff changeset
    87
  | read report scanner (syms, pos) =
30590
1d9c9fcf8513 parameterized datatype antiquote and read operation;
wenzelm
parents: 30589
diff changeset
    88
      (case Scan.read Symbol_Pos.stopper (Scan.repeat scanner) syms of
30613
b22d35d9ef28 Antiquote.read: argument for reporting text;
wenzelm
parents: 30590
diff changeset
    89
        SOME xs =>
b22d35d9ef28 Antiquote.read: argument for reporting text;
wenzelm
parents: 30590
diff changeset
    90
         (List.app (fn Antiq (_, pos) => Position.report Markup.antiq pos | Text x => report x) xs;
b22d35d9ef28 Antiquote.read: argument for reporting text;
wenzelm
parents: 30590
diff changeset
    91
          check_nesting xs; xs)
27767
b52c0c81dcf3 renamed scan_antiquotes to read;
wenzelm
parents: 27750
diff changeset
    92
      | 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
    93
6a4fae41a75f Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff changeset
    94
end;