src/Pure/PIDE/command_span.ML

separate module Command_Span: mostly syntactic representation;
potentially prover-specific Output_Syntax.parse_spans;

(*  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
  val resolve_files: (string -> Path.T * Position.T -> Token.file Exn.result list) -> span -> span
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;


(* resolve inlined files *)

local

fun clean ((i1, t1) :: (i2, t2) :: toks) =
      if Token.keyword_with (fn s => s = "%" orelse s = "--") t1 then clean toks
      else (i1, t1) :: clean ((i2, t2) :: toks)
  | clean toks = toks;

fun clean_tokens toks =
  ((0 upto length toks - 1) ~~ toks)
  |> filter (fn (_, tok) => Token.is_proper tok)
  |> clean;

fun find_file ((_, tok) :: toks) =
      if Token.is_command tok then
        toks |> get_first (fn (i, tok) =>
          if Token.is_name tok then
            SOME (i, (Path.explode (Token.content_of tok), Token.pos_of tok))
              handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok))
          else NONE)
      else NONE
  | find_file [] = NONE;

in

fun resolve_files read_files span =
  (case span of
    Span (Command_Span (cmd, pos), toks) =>
      if Keyword.is_theory_load cmd then
        (case find_file (clean_tokens toks) of
          NONE => error ("Bad file argument of command " ^ quote cmd ^ Position.here pos)
        | SOME (i, path) =>
            let
              val toks' = toks |> map_index (fn (j, tok) =>
                if i = j then Token.put_files (read_files cmd path) tok
                else tok);
            in Span (Command_Span (cmd, pos), toks') end)
      else span
  | _ => span);

end;

end;