src/Pure/PIDE/command_span.ML
author wenzelm
Sun Mar 10 14:19:30 2019 +0100 (4 months ago ago)
changeset 70070 be04e9a053a7
parent 68184 6560324b1e4d
permissions -rw-r--r--
markup and document markers for some meta data from "Dublin Core Metadata Element Set";
wenzelm@57905
     1
(*  Title:      Pure/PIDE/command_span.ML
wenzelm@57905
     2
    Author:     Makarius
wenzelm@57905
     3
wenzelm@57905
     4
Syntactic representation of command spans.
wenzelm@57905
     5
*)
wenzelm@57905
     6
wenzelm@57905
     7
signature COMMAND_SPAN =
wenzelm@57905
     8
sig
wenzelm@57905
     9
  datatype kind = Command_Span of string * Position.T | Ignored_Span | Malformed_Span
wenzelm@57905
    10
  datatype span = Span of kind * Token.T list
wenzelm@57905
    11
  val kind: span -> kind
wenzelm@57905
    12
  val content: span -> Token.T list
wenzelm@68184
    13
  val symbol_length: span -> int option
wenzelm@68184
    14
  val adjust_offsets_kind: (int -> int option) -> kind -> kind
wenzelm@68184
    15
  val adjust_offsets: (int -> int option) -> span -> span
wenzelm@57905
    16
end;
wenzelm@57905
    17
wenzelm@57905
    18
structure Command_Span: COMMAND_SPAN =
wenzelm@57905
    19
struct
wenzelm@57905
    20
wenzelm@57905
    21
datatype kind = Command_Span of string * Position.T | Ignored_Span | Malformed_Span;
wenzelm@57905
    22
datatype span = Span of kind * Token.T list;
wenzelm@57905
    23
wenzelm@57905
    24
fun kind (Span (k, _)) = k;
wenzelm@57905
    25
fun content (Span (_, toks)) = toks;
wenzelm@68184
    26
val symbol_length = Position.distance_of o Token.range_of o content;
wenzelm@68178
    27
wenzelm@68184
    28
fun adjust_offsets_kind adjust k =
wenzelm@68184
    29
  (case k of
wenzelm@68184
    30
    Command_Span (name, pos) => Command_Span (name, Position.adjust_offsets adjust pos)
wenzelm@68184
    31
  | _ => k);
wenzelm@68184
    32
wenzelm@68184
    33
fun adjust_offsets adjust (Span (k, toks)) =
wenzelm@68184
    34
  Span (adjust_offsets_kind adjust k, map (Token.adjust_offsets adjust) toks);
wenzelm@68178
    35
wenzelm@57905
    36
end;