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