src/Pure/PIDE/command_span.ML
author wenzelm
Mon Mar 13 21:37:35 2017 +0100 (2017-03-13 ago)
changeset 65214 a2ec0db555c7
parent 59689 7968c57ea240
child 68178 6e40f5d43936
permissions -rw-r--r--
clarified modules;
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@57905
    13
end;
wenzelm@57905
    14
wenzelm@57905
    15
structure Command_Span: COMMAND_SPAN =
wenzelm@57905
    16
struct
wenzelm@57905
    17
wenzelm@57905
    18
datatype kind = Command_Span of string * Position.T | Ignored_Span | Malformed_Span;
wenzelm@57905
    19
datatype span = Span of kind * Token.T list;
wenzelm@57905
    20
wenzelm@57905
    21
fun kind (Span (k, _)) = k;
wenzelm@57905
    22
fun content (Span (_, toks)) = toks;
wenzelm@57905
    23
wenzelm@57905
    24
end;