src/Pure/General/symbol_pos.ML
author wenzelm
Thu Aug 07 19:21:40 2008 +0200 (2008-08-07)
changeset 27778 3ec7a4d9ef18
parent 27763 f49f6275cefa
child 27797 9861b39a2fd5
permissions -rw-r--r--
renamed SymbolPos.scan_position to SymbolPos.scan_pos;
implode/explode: explicit type text = string;
added implode_delim;
explode: Position.reset_range;
wenzelm@27763
     1
(*  Title:      Pure/General/symbol_pos.ML
wenzelm@27763
     2
    ID:         $Id$
wenzelm@27763
     3
    Author:     Makarius
wenzelm@27763
     4
wenzelm@27763
     5
Symbols with explicit position information.
wenzelm@27763
     6
*)
wenzelm@27763
     7
wenzelm@27763
     8
signature BASIC_SYMBOL_POS =
wenzelm@27763
     9
sig
wenzelm@27763
    10
  type T = Symbol.symbol * Position.T
wenzelm@27763
    11
  val symbol: T -> Symbol.symbol
wenzelm@27763
    12
  val $$$ : Symbol.symbol -> T list -> T list * T list
wenzelm@27763
    13
  val ~$$$ : Symbol.symbol -> T list -> T list * T list
wenzelm@27763
    14
end
wenzelm@27763
    15
wenzelm@27763
    16
signature SYMBOL_POS =
wenzelm@27763
    17
sig
wenzelm@27763
    18
  include BASIC_SYMBOL_POS
wenzelm@27763
    19
  val is_eof: T -> bool
wenzelm@27763
    20
  val stopper: T Scan.stopper
wenzelm@27763
    21
  val !!! : string -> (T list -> 'a) -> T list -> 'a
wenzelm@27778
    22
  val scan_pos: T list -> Position.T * T list
wenzelm@27763
    23
  val scan_comment: (string -> (T list -> T list * T list) -> T list -> T list * T list) ->
wenzelm@27763
    24
    T list -> T list * T list
wenzelm@27763
    25
  val scan_comment_body: (string -> (T list -> T list * T list) -> T list -> T list * T list) ->
wenzelm@27763
    26
    T list -> T list * T list
wenzelm@27763
    27
  val source: Position.T -> (Symbol.symbol, 'a) Source.source ->
wenzelm@27763
    28
    (T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source
wenzelm@27778
    29
  type text = string
wenzelm@27778
    30
  val implode: T list -> text * Position.range
wenzelm@27778
    31
  val implode_delim: Position.T -> Position.T -> T list -> text * Position.range
wenzelm@27778
    32
  val explode: text * Position.T -> T list
wenzelm@27763
    33
end;
wenzelm@27763
    34
wenzelm@27763
    35
structure SymbolPos: SYMBOL_POS =
wenzelm@27763
    36
struct
wenzelm@27763
    37
wenzelm@27763
    38
(* type T *)
wenzelm@27763
    39
wenzelm@27763
    40
type T = Symbol.symbol * Position.T;
wenzelm@27763
    41
wenzelm@27763
    42
fun symbol ((s, _): T) = s;
wenzelm@27763
    43
wenzelm@27763
    44
wenzelm@27763
    45
(* stopper *)
wenzelm@27763
    46
wenzelm@27763
    47
fun mk_eof pos = (Symbol.eof, pos);
wenzelm@27763
    48
val eof = mk_eof Position.none;
wenzelm@27763
    49
wenzelm@27763
    50
val is_eof = Symbol.is_eof o symbol;
wenzelm@27763
    51
wenzelm@27763
    52
val stopper =
wenzelm@27763
    53
  Scan.stopper (fn [] => eof | inp => mk_eof (List.last inp |-> Position.advance)) is_eof;
wenzelm@27763
    54
wenzelm@27763
    55
wenzelm@27763
    56
(* basic scanners *)
wenzelm@27763
    57
wenzelm@27763
    58
fun !!! text scan =
wenzelm@27763
    59
  let
wenzelm@27763
    60
    fun get_pos [] = " (past end-of-text!)"
wenzelm@27763
    61
      | get_pos ((_, pos) :: _) = Position.str_of pos;
wenzelm@27763
    62
wenzelm@27763
    63
    fun err (syms, msg) =
wenzelm@27763
    64
      text ^ get_pos syms ^ " at " ^ Symbol.beginning 10 (map symbol syms) ^
wenzelm@27763
    65
      (case msg of NONE => "" | SOME s => "\n" ^ s);
wenzelm@27763
    66
  in Scan.!! err scan end;
wenzelm@27763
    67
wenzelm@27763
    68
fun $$$ s = Scan.one (fn x => symbol x = s) >> single;
wenzelm@27763
    69
fun ~$$$ s = Scan.one (fn x => symbol x <> s) >> single;
wenzelm@27763
    70
wenzelm@27778
    71
val scan_pos = Scan.ahead (Scan.one (K true)) >> (fn (_, pos): T => pos);
wenzelm@27763
    72
wenzelm@27763
    73
wenzelm@27763
    74
(* ML-style comments *)
wenzelm@27763
    75
wenzelm@27763
    76
local
wenzelm@27763
    77
wenzelm@27763
    78
val scan_cmt =
wenzelm@27763
    79
  Scan.depend (fn (d: int) => $$$ "(" @@@ $$$ "*" >> pair (d + 1)) ||
wenzelm@27763
    80
  Scan.depend (fn 0 => Scan.fail | d => $$$ "*" @@@ $$$ ")" >> pair (d - 1)) ||
wenzelm@27763
    81
  Scan.lift ($$$ "*" --| Scan.ahead (~$$$ ")")) ||
wenzelm@27763
    82
  Scan.lift (Scan.one (fn (s, _) => s <> "*" andalso Symbol.is_regular s)) >> single;
wenzelm@27763
    83
wenzelm@27763
    84
val scan_body = Scan.pass 0 (Scan.repeat scan_cmt >> flat);
wenzelm@27763
    85
wenzelm@27763
    86
in
wenzelm@27763
    87
wenzelm@27763
    88
fun scan_comment cut =
wenzelm@27763
    89
  $$$ "(" @@@ $$$ "*" @@@ cut "missing end of comment" (scan_body @@@ $$$ "*" @@@ $$$ ")");
wenzelm@27763
    90
wenzelm@27763
    91
fun scan_comment_body cut =
wenzelm@27763
    92
  $$$ "(" |-- $$$ "*" |-- cut "missing end of comment" (scan_body --| $$$ "*" --| $$$ ")");
wenzelm@27763
    93
wenzelm@27763
    94
end;
wenzelm@27763
    95
wenzelm@27763
    96
wenzelm@27763
    97
(* source *)
wenzelm@27763
    98
wenzelm@27763
    99
fun source pos =
wenzelm@27763
   100
  Source.source' pos Symbol.stopper (Scan.bulk (Scan.depend (fn pos =>
wenzelm@27763
   101
    Scan.one Symbol.not_eof >> (fn s => (Position.advance s pos, (s, pos)))))) NONE;
wenzelm@27763
   102
wenzelm@27763
   103
wenzelm@27763
   104
(* compact representation -- with Symbol.DEL padding *)
wenzelm@27763
   105
wenzelm@27778
   106
type text = string;
wenzelm@27778
   107
wenzelm@27763
   108
local
wenzelm@27763
   109
wenzelm@27763
   110
fun pad [] = []
wenzelm@27763
   111
  | pad [(s, _)] = [s]
wenzelm@27763
   112
  | pad ((s1, pos1) :: (rest as (s2, pos2) :: _)) =
wenzelm@27763
   113
      let
wenzelm@27763
   114
        fun err () =
wenzelm@27763
   115
          raise Fail ("Misaligned symbols: " ^
wenzelm@27763
   116
            quote s1 ^ Position.str_of pos1 ^ " " ^
wenzelm@27763
   117
            quote s2 ^ Position.str_of pos2);
wenzelm@27763
   118
wenzelm@27763
   119
        val end_pos1 = Position.advance s1 pos1;
wenzelm@27763
   120
        val _ = Position.line_of end_pos1 = Position.line_of pos2 orelse err ();
wenzelm@27763
   121
        val d =
wenzelm@27763
   122
          (case (Position.column_of end_pos1, Position.column_of pos2) of
wenzelm@27763
   123
            (NONE, NONE) => 0
wenzelm@27763
   124
          | (SOME n1, SOME n2) => n2 - n1
wenzelm@27763
   125
          | _ => err ());
wenzelm@27763
   126
        val _ = d >= 0 orelse err ();
wenzelm@27763
   127
      in s1 :: replicate d Symbol.DEL @ pad rest end;
wenzelm@27763
   128
wenzelm@27763
   129
val orig_implode = implode;
wenzelm@27763
   130
wenzelm@27763
   131
in
wenzelm@27763
   132
wenzelm@27763
   133
fun implode (syms as (_, pos) :: _) =
wenzelm@27763
   134
      let val pos' = List.last syms |-> Position.advance
wenzelm@27763
   135
      in (orig_implode (pad syms), Position.range pos pos') end
wenzelm@27763
   136
  | implode [] = ("", (Position.none, Position.none));
wenzelm@27763
   137
wenzelm@27778
   138
fun implode_delim pos1 pos2 syms = implode (("", pos1) :: syms @ [("", pos2)]);
wenzelm@27778
   139
wenzelm@27763
   140
fun explode (str, pos) =
wenzelm@27778
   141
  fold_map (fn s => fn p => ((s, p), (Position.advance s p)))
wenzelm@27778
   142
    (Symbol.explode str) (Position.reset_range pos)
wenzelm@27763
   143
  |> #1 |> filter_out (fn (s, _) => s = Symbol.DEL);
wenzelm@27763
   144
wenzelm@27763
   145
end;
wenzelm@27763
   146
wenzelm@27763
   147
end;
wenzelm@27763
   148
wenzelm@27763
   149
structure BasicSymbolPos: BASIC_SYMBOL_POS = SymbolPos;   (*not open by default*)
wenzelm@27763
   150