src/Pure/PIDE/command_span.ML
author wenzelm
Tue Aug 12 18:36:43 2014 +0200 (2014-08-12)
changeset 57916 2c2c24dbf0a4
parent 57905 c0c5652e796e
child 58923 cb9b69cca999
permissions -rw-r--r--
generic process wrapping in Prover;
clarified module arrangement;
     1 (*  Title:      Pure/PIDE/command_span.ML
     2     Author:     Makarius
     3 
     4 Syntactic representation of command spans.
     5 *)
     6 
     7 signature COMMAND_SPAN =
     8 sig
     9   datatype kind = Command_Span of string * Position.T | Ignored_Span | Malformed_Span
    10   datatype span = Span of kind * Token.T list
    11   val kind: span -> kind
    12   val content: span -> Token.T list
    13   val resolve_files: (string -> Path.T * Position.T -> Token.file Exn.result list) -> span -> span
    14 end;
    15 
    16 structure Command_Span: COMMAND_SPAN =
    17 struct
    18 
    19 datatype kind = Command_Span of string * Position.T | Ignored_Span | Malformed_Span;
    20 datatype span = Span of kind * Token.T list;
    21 
    22 fun kind (Span (k, _)) = k;
    23 fun content (Span (_, toks)) = toks;
    24 
    25 
    26 (* resolve inlined files *)
    27 
    28 local
    29 
    30 fun clean ((i1, t1) :: (i2, t2) :: toks) =
    31       if Token.keyword_with (fn s => s = "%" orelse s = "--") t1 then clean toks
    32       else (i1, t1) :: clean ((i2, t2) :: toks)
    33   | clean toks = toks;
    34 
    35 fun clean_tokens toks =
    36   ((0 upto length toks - 1) ~~ toks)
    37   |> filter (fn (_, tok) => Token.is_proper tok)
    38   |> clean;
    39 
    40 fun find_file ((_, tok) :: toks) =
    41       if Token.is_command tok then
    42         toks |> get_first (fn (i, tok) =>
    43           if Token.is_name tok then
    44             SOME (i, (Path.explode (Token.content_of tok), Token.pos_of tok))
    45               handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok))
    46           else NONE)
    47       else NONE
    48   | find_file [] = NONE;
    49 
    50 in
    51 
    52 fun resolve_files read_files span =
    53   (case span of
    54     Span (Command_Span (cmd, pos), toks) =>
    55       if Keyword.is_theory_load cmd then
    56         (case find_file (clean_tokens toks) of
    57           NONE => error ("Bad file argument of command " ^ quote cmd ^ Position.here pos)
    58         | SOME (i, path) =>
    59             let
    60               val toks' = toks |> map_index (fn (j, tok) =>
    61                 if i = j then Token.put_files (read_files cmd path) tok
    62                 else tok);
    63             in Span (Command_Span (cmd, pos), toks') end)
    64       else span
    65   | _ => span);
    66 
    67 end;
    68 
    69 end;
    70