src/Pure/PIDE/command_span.ML
author wenzelm
Mon, 03 Apr 2017 14:29:44 +0200
changeset 65358 e345e9420109
parent 59689 7968c57ea240
child 68177 6e40f5d43936
permissions -rw-r--r--
proper qualifier (again, see df4cd6e1fdfa);

(*  Title:      Pure/PIDE/command_span.ML
    Author:     Makarius

Syntactic representation of command spans.
*)

signature COMMAND_SPAN =
sig
  datatype kind = Command_Span of string * Position.T | Ignored_Span | Malformed_Span
  datatype span = Span of kind * Token.T list
  val kind: span -> kind
  val content: span -> Token.T list
end;

structure Command_Span: COMMAND_SPAN =
struct

datatype kind = Command_Span of string * Position.T | Ignored_Span | Malformed_Span;
datatype span = Span of kind * Token.T list;

fun kind (Span (k, _)) = k;
fun content (Span (_, toks)) = toks;

end;