src/Pure/PIDE/command_span.ML
author wenzelm
Wed Dec 03 14:04:38 2014 +0100 (2014-12-03 ago)
changeset 59083 88b0b1f28adc
parent 58923 cb9b69cca999
child 59683 d6824d8490be
permissions -rw-r--r--
tuned signature;
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@58923
    13
  val resolve_files: Keyword.keywords ->
wenzelm@58923
    14
    (string -> Path.T * Position.T -> Token.file Exn.result list) -> span -> span
wenzelm@57905
    15
end;
wenzelm@57905
    16
wenzelm@57905
    17
structure Command_Span: COMMAND_SPAN =
wenzelm@57905
    18
struct
wenzelm@57905
    19
wenzelm@57905
    20
datatype kind = Command_Span of string * Position.T | Ignored_Span | Malformed_Span;
wenzelm@57905
    21
datatype span = Span of kind * Token.T list;
wenzelm@57905
    22
wenzelm@57905
    23
fun kind (Span (k, _)) = k;
wenzelm@57905
    24
fun content (Span (_, toks)) = toks;
wenzelm@57905
    25
wenzelm@57905
    26
wenzelm@57905
    27
(* resolve inlined files *)
wenzelm@57905
    28
wenzelm@57905
    29
local
wenzelm@57905
    30
wenzelm@57905
    31
fun clean ((i1, t1) :: (i2, t2) :: toks) =
wenzelm@57905
    32
      if Token.keyword_with (fn s => s = "%" orelse s = "--") t1 then clean toks
wenzelm@57905
    33
      else (i1, t1) :: clean ((i2, t2) :: toks)
wenzelm@57905
    34
  | clean toks = toks;
wenzelm@57905
    35
wenzelm@57905
    36
fun clean_tokens toks =
wenzelm@57905
    37
  ((0 upto length toks - 1) ~~ toks)
wenzelm@57905
    38
  |> filter (fn (_, tok) => Token.is_proper tok)
wenzelm@57905
    39
  |> clean;
wenzelm@57905
    40
wenzelm@57905
    41
fun find_file ((_, tok) :: toks) =
wenzelm@57905
    42
      if Token.is_command tok then
wenzelm@57905
    43
        toks |> get_first (fn (i, tok) =>
wenzelm@57905
    44
          if Token.is_name tok then
wenzelm@57905
    45
            SOME (i, (Path.explode (Token.content_of tok), Token.pos_of tok))
wenzelm@57905
    46
              handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok))
wenzelm@57905
    47
          else NONE)
wenzelm@57905
    48
      else NONE
wenzelm@57905
    49
  | find_file [] = NONE;
wenzelm@57905
    50
wenzelm@57905
    51
in
wenzelm@57905
    52
wenzelm@58923
    53
fun resolve_files keywords read_files span =
wenzelm@57905
    54
  (case span of
wenzelm@57905
    55
    Span (Command_Span (cmd, pos), toks) =>
wenzelm@58923
    56
      if Keyword.is_theory_load keywords cmd then
wenzelm@57905
    57
        (case find_file (clean_tokens toks) of
wenzelm@57905
    58
          NONE => error ("Bad file argument of command " ^ quote cmd ^ Position.here pos)
wenzelm@57905
    59
        | SOME (i, path) =>
wenzelm@57905
    60
            let
wenzelm@57905
    61
              val toks' = toks |> map_index (fn (j, tok) =>
wenzelm@57905
    62
                if i = j then Token.put_files (read_files cmd path) tok
wenzelm@57905
    63
                else tok);
wenzelm@57905
    64
            in Span (Command_Span (cmd, pos), toks') end)
wenzelm@57905
    65
      else span
wenzelm@57905
    66
  | _ => span);
wenzelm@57905
    67
wenzelm@57905
    68
end;
wenzelm@57905
    69
wenzelm@57905
    70
end;
wenzelm@57905
    71