src/Pure/PIDE/command.ML
changeset 72841 fd8d82c4433b
parent 72747 5f9d66155081
child 72945 756b9cb8a176
equal deleted inserted replaced
72840:6b96464066a0 72841:fd8d82c4433b
     5 *)
     5 *)
     6 
     6 
     7 signature COMMAND =
     7 signature COMMAND =
     8 sig
     8 sig
     9   type blob = {file_node: string, src_path: Path.T, content: (SHA1.digest * string list) option}
     9   type blob = {file_node: string, src_path: Path.T, content: (SHA1.digest * string list) option}
    10   val read_file: Path.T -> Position.T -> Path.T -> Token.file
    10   val read_file: Path.T -> Position.T -> bool -> Path.T -> Token.file
    11   val read_thy: Toplevel.state -> theory
    11   val read_thy: Toplevel.state -> theory
    12   val read: Keyword.keywords -> theory -> Path.T-> (unit -> theory) ->
    12   val read: Keyword.keywords -> theory -> Path.T-> (unit -> theory) ->
    13     blob Exn.result list * int -> Token.T list -> Toplevel.transition
    13     blob Exn.result list * int -> Token.T list -> Toplevel.transition
    14   type eval
    14   type eval
    15   val eval_command_id: eval -> Document_ID.command
    15   val eval_command_id: eval -> Document_ID.command
    53 
    53 
    54 (* read *)
    54 (* read *)
    55 
    55 
    56 type blob = {file_node: string, src_path: Path.T, content: (SHA1.digest * string list) option};
    56 type blob = {file_node: string, src_path: Path.T, content: (SHA1.digest * string list) option};
    57 
    57 
    58 fun read_file_node file_node master_dir pos src_path =
    58 fun read_file_node file_node master_dir pos delimited src_path =
    59   let
    59   let
    60     val _ =
    60     val _ =
    61       if Context_Position.pide_reports ()
    61       if Context_Position.pide_reports ()
    62       then Position.report pos Markup.language_path else ();
    62       then Position.report pos (Markup.language_path delimited) else ();
    63     val _ =
    63     val _ =
    64       (case try Url.explode file_node of
    64       (case try Url.explode file_node of
    65         NONE => ()
    65         NONE => ()
    66       | SOME (Url.File _) => ()
    66       | SOME (Url.File _) => ()
    67       | _ =>
    67       | _ =>
    88       | SOME exec_id => Position.put_id exec_id);
    88       | SOME exec_id => Position.put_id exec_id);
    89   in {src_path = src_path, lines = lines, digest = digest, pos = file_pos} end
    89   in {src_path = src_path, lines = lines, digest = digest, pos = file_pos} end
    90 
    90 
    91 fun resolve_files master_dir (blobs, blobs_index) toks =
    91 fun resolve_files master_dir (blobs, blobs_index) toks =
    92   (case Outer_Syntax.parse_spans toks of
    92   (case Outer_Syntax.parse_spans toks of
    93     [Command_Span.Span (Command_Span.Command_Span (cmd, _), _)] =>
    93     [Command_Span.Span (Command_Span.Command_Span _, _)] =>
    94       (case try (nth toks) blobs_index of
    94       (case try (nth toks) blobs_index of
    95         SOME tok =>
    95         SOME tok =>
    96           let
    96           let
    97             val pos = Token.pos_of tok;
    97             val source = Token.input_of tok;
       
    98             val pos = Input.pos_of source;
       
    99             val delimited = Input.is_delimited source;
       
   100 
    98             fun make_file (Exn.Res {file_node, src_path, content = NONE}) =
   101             fun make_file (Exn.Res {file_node, src_path, content = NONE}) =
    99                   Exn.interruptible_capture (fn () =>
   102                   Exn.interruptible_capture (fn () =>
   100                     read_file_node file_node master_dir pos src_path) ()
   103                     read_file_node file_node master_dir pos delimited src_path) ()
   101               | make_file (Exn.Res {file_node, src_path, content = SOME (digest, lines)}) =
   104               | make_file (Exn.Res {file_node, src_path, content = SOME (digest, lines)}) =
   102                   (Position.report pos Markup.language_path;
   105                   (Position.report pos (Markup.language_path delimited);
   103                     Exn.Res (blob_file src_path lines digest file_node))
   106                     Exn.Res (blob_file src_path lines digest file_node))
   104               | make_file (Exn.Exn e) = Exn.Exn e;
   107               | make_file (Exn.Exn e) = Exn.Exn e;
   105             val files = map make_file blobs;
   108             val files = map make_file blobs;
   106           in
   109           in
   107             toks |> map_index (fn (i, tok) =>
   110             toks |> map_index (fn (i, tok) =>