src/Pure/Isar/antiquote.ML
author wenzelm
Thu Aug 07 13:44:56 2008 +0200 (2008-08-07)
changeset 27767 b52c0c81dcf3
parent 27750 7f5fb39c6362
child 27779 4569003b8813
permissions -rw-r--r--
renamed scan_antiquotes to read;
renamed scan_arguments to read_arguments;
improved position handling due to SymbolPos.T;
tuned;
wenzelm@9138
     1
(*  Title:      Pure/Isar/antiquote.ML
wenzelm@9138
     2
    ID:         $Id$
wenzelm@9138
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@9138
     4
wenzelm@9138
     5
Text with antiquotations of inner items (terms, types etc.).
wenzelm@9138
     6
*)
wenzelm@9138
     7
wenzelm@9138
     8
signature ANTIQUOTE =
wenzelm@9138
     9
sig
wenzelm@27342
    10
  datatype antiquote =
wenzelm@27750
    11
    Text of string | Antiq of (string * Position.T) * Position.T |
wenzelm@27342
    12
    Open of Position.T | Close of Position.T
wenzelm@9138
    13
  val is_antiq: antiquote -> bool
wenzelm@27767
    14
  val read: string * Position.T -> antiquote list
wenzelm@27767
    15
  val read_arguments: Scan.lexicon -> (OuterLex.token list -> 'a * OuterLex.token list) ->
wenzelm@22114
    16
    string * Position.T -> 'a
wenzelm@9138
    17
end;
wenzelm@9138
    18
wenzelm@9138
    19
structure Antiquote: ANTIQUOTE =
wenzelm@9138
    20
struct
wenzelm@9138
    21
wenzelm@9138
    22
(* datatype antiquote *)
wenzelm@9138
    23
wenzelm@9138
    24
datatype antiquote =
wenzelm@9138
    25
  Text of string |
wenzelm@27750
    26
  Antiq of (string * Position.T) * Position.T (*text, inner position, outer position*) |
wenzelm@27342
    27
  Open of Position.T |
wenzelm@27342
    28
  Close of Position.T;
wenzelm@9138
    29
wenzelm@9138
    30
fun is_antiq (Text _) = false
wenzelm@27342
    31
  | is_antiq _ = true;
wenzelm@27342
    32
wenzelm@27342
    33
wenzelm@27342
    34
(* check_nesting *)
wenzelm@27342
    35
wenzelm@27342
    36
fun err_unbalanced pos =
wenzelm@27342
    37
  error ("Unbalanced antiquotation block parentheses" ^ Position.str_of pos);
wenzelm@27342
    38
wenzelm@27342
    39
fun check_nesting antiqs =
wenzelm@27342
    40
  let
wenzelm@27342
    41
    fun check [] [] = ()
wenzelm@27342
    42
      | check [] (pos :: _) = err_unbalanced pos
wenzelm@27342
    43
      | check (Open pos :: ants) ps = check ants (pos :: ps)
wenzelm@27342
    44
      | check (Close pos :: _) [] = err_unbalanced pos
wenzelm@27342
    45
      | check (Close _ :: ants) (_ :: ps) = check ants ps
wenzelm@27342
    46
      | check (_ :: ants) ps = check ants ps;
wenzelm@27342
    47
  in check antiqs [] end;
wenzelm@9138
    48
wenzelm@9138
    49
wenzelm@9138
    50
(* scan_antiquote *)
wenzelm@9138
    51
wenzelm@27767
    52
open BasicSymbolPos;
wenzelm@22114
    53
structure T = OuterLex;
wenzelm@9138
    54
wenzelm@22114
    55
local
wenzelm@9138
    56
wenzelm@9138
    57
val scan_txt =
wenzelm@27767
    58
  $$$ "@" --| Scan.ahead (~$$$ "{") ||
wenzelm@27767
    59
  Scan.one (fn (s, _) => s <> "@" andalso s <> "\\<lbrace>" andalso s <> "\\<rbrace>"
wenzelm@27767
    60
    andalso Symbol.is_regular s) >> single;
wenzelm@9138
    61
wenzelm@9138
    62
val scan_ant =
wenzelm@27767
    63
  T.scan_quoted ||
wenzelm@27767
    64
  Scan.one (fn (s, _) => s <> "}" andalso Symbol.is_regular s) >> single;
wenzelm@9138
    65
wenzelm@9138
    66
val scan_antiq =
wenzelm@27767
    67
  SymbolPos.scan_position -- ($$$ "@" |-- $$$ "{" |--
wenzelm@9138
    68
    T.!!! "missing closing brace of antiquotation"
wenzelm@27767
    69
      (SymbolPos.scan_position -- Scan.repeat scan_ant -- SymbolPos.scan_position --
wenzelm@27767
    70
        ($$$ "}" |-- SymbolPos.scan_position)))
wenzelm@27750
    71
  >> (fn (pos1, (((pos2, body), pos3), pos4)) =>
wenzelm@27767
    72
    Antiq ((implode (map symbol (flat body)),
wenzelm@27767
    73
      Position.encode_range (pos2, pos3)), Position.encode_range (pos1, pos4)));
wenzelm@9138
    74
wenzelm@9138
    75
in
wenzelm@9138
    76
wenzelm@27767
    77
val scan_antiquote = T.!!! "malformed quotation/antiquotation"
wenzelm@27767
    78
 (Scan.repeat1 scan_txt >> (Text o implode o map symbol o flat) ||
wenzelm@27750
    79
  scan_antiq ||
wenzelm@27767
    80
  SymbolPos.scan_position --| $$$ "\\<lbrace>" >> Open ||
wenzelm@27767
    81
  SymbolPos.scan_position --| $$$ "\\<rbrace>" >> Close);
wenzelm@9138
    82
wenzelm@9138
    83
end;
wenzelm@9138
    84
wenzelm@9138
    85
wenzelm@27767
    86
(* read *)
wenzelm@9138
    87
wenzelm@27767
    88
fun read ("", _) = []
wenzelm@27767
    89
  | read (s, pos) =
wenzelm@27767
    90
      (case Scan.read SymbolPos.stopper (Scan.bulk scan_antiquote) (SymbolPos.explode (s, pos)) of
wenzelm@27767
    91
        SOME xs => (check_nesting xs; xs)
wenzelm@27767
    92
      | NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos));
wenzelm@9138
    93
wenzelm@9138
    94
wenzelm@22114
    95
(* scan_arguments *)
wenzelm@22114
    96
wenzelm@27767
    97
fun read_arguments lex scan (s, pos) =
wenzelm@22114
    98
  let
wenzelm@22114
    99
    fun err msg = cat_error msg
wenzelm@22114
   100
      ("Malformed antiquotation: " ^ quote ("@{" ^ s ^ "}") ^ Position.str_of pos);
wenzelm@22114
   101
wenzelm@22114
   102
    val res =
wenzelm@22114
   103
      Source.of_string s
wenzelm@22114
   104
      |> Symbol.source false
wenzelm@23677
   105
      |> T.source NONE (K (lex, Scan.empty_lexicon)) pos
wenzelm@22114
   106
      |> T.source_proper
wenzelm@27767
   107
      |> Source.source T.stopper (Scan.error (Scan.bulk scan)) NONE
wenzelm@22114
   108
      |> Source.exhaust;
wenzelm@22114
   109
  in (case res of [x] => x | _ => err "") handle ERROR msg => err msg end;
wenzelm@22114
   110
wenzelm@9138
   111
end;