src/Pure/PIDE/command.ML
changeset 55788 67699e08e969
parent 55709 4e5a83a46ded
child 55798 985bd3a325ab
     1.1 --- a/src/Pure/PIDE/command.ML	Thu Feb 27 17:24:46 2014 +0100
     1.2 +++ b/src/Pure/PIDE/command.ML	Thu Feb 27 17:29:58 2014 +0100
     1.3 @@ -6,15 +6,17 @@
     1.4  
     1.5  signature COMMAND =
     1.6  sig
     1.7 -  type blob = (string * string option) Exn.result
     1.8 +  type 'a blob = (string * 'a option) Exn.result
     1.9 +  type blob_digest = string blob
    1.10 +  type content = SHA1.digest * string list
    1.11    val read_file: Path.T -> Position.T -> Path.T -> Token.file
    1.12 -  val read: (unit -> theory) -> Path.T -> blob list -> Token.T list -> Toplevel.transition
    1.13 +  val read: (unit -> theory) -> Path.T -> content blob list -> Token.T list -> Toplevel.transition
    1.14    type eval
    1.15    val eval_eq: eval * eval -> bool
    1.16    val eval_running: eval -> bool
    1.17    val eval_finished: eval -> bool
    1.18    val eval_result_state: eval -> Toplevel.state
    1.19 -  val eval: (unit -> theory) -> Path.T -> blob list -> Token.T list -> eval -> eval
    1.20 +  val eval: (unit -> theory) -> Path.T -> content blob list -> Token.T list -> eval -> eval
    1.21    type print
    1.22    val print: bool -> (string * string list) list -> string ->
    1.23      eval -> print list -> print list option
    1.24 @@ -86,13 +88,29 @@
    1.25  
    1.26  (* read *)
    1.27  
    1.28 -type blob = (string * string option) Exn.result;  (*file node name, digest or text*)
    1.29 +type 'a blob = (string * 'a option) Exn.result;  (*file node name, content*)
    1.30 +type blob_digest = string blob;  (*raw digest*)
    1.31 +type content = SHA1.digest * string list;  (*digest, lines*)
    1.32  
    1.33  fun read_file master_dir pos src_path =
    1.34    let
    1.35      val full_path = File.check_file (File.full_path master_dir src_path);
    1.36      val _ = Position.report pos (Markup.path (Path.implode full_path));
    1.37 -  in {src_path = src_path, text = File.read full_path, pos = Path.position full_path} end;
    1.38 +    val text = File.read full_path;
    1.39 +    val lines = split_lines text;
    1.40 +    val digest = SHA1.digest text;
    1.41 +  in {src_path = src_path, lines = lines, digest = digest, pos = Path.position full_path} end;
    1.42 +
    1.43 +local
    1.44 +
    1.45 +fun blob_file src_path file (digest, lines) =
    1.46 +  let
    1.47 +    val file_pos =
    1.48 +      Position.file file (*sic!*) |>
    1.49 +      (case Position.get_id (Position.thread_data ()) of
    1.50 +        NONE => I
    1.51 +      | SOME exec_id => Position.put_id exec_id);
    1.52 +  in {src_path = src_path, lines = lines, digest = digest, pos = file_pos} end
    1.53  
    1.54  fun resolve_files master_dir blobs toks =
    1.55    (case Thy_Syntax.parse_spans toks of
    1.56 @@ -101,17 +119,10 @@
    1.57          let
    1.58            fun make_file src_path (Exn.Res (_, NONE)) =
    1.59                  Exn.interruptible_capture (fn () => read_file master_dir pos src_path) ()
    1.60 -            | make_file src_path (Exn.Res (file, SOME text)) =
    1.61 -                let
    1.62 -                  val _ = Position.report pos (Markup.path file);
    1.63 -                  val file_pos =
    1.64 -                    Position.file file (*sic!*) |>
    1.65 -                    (case Position.get_id (Position.thread_data ()) of
    1.66 -                      NONE => I
    1.67 -                    | SOME exec_id => Position.put_id exec_id);
    1.68 -                in Exn.Res {src_path = src_path, text = text, pos = file_pos} end
    1.69 +            | make_file src_path (Exn.Res (file, SOME content)) =
    1.70 +               (Position.report pos (Markup.path file);
    1.71 +                Exn.Res (blob_file src_path file content))
    1.72              | make_file _ (Exn.Exn e) = Exn.Exn e;
    1.73 -
    1.74            val src_paths = Keyword.command_files cmd path;
    1.75          in
    1.76            if null blobs then
    1.77 @@ -123,6 +134,8 @@
    1.78        |> Thy_Syntax.span_content
    1.79    | _ => toks);
    1.80  
    1.81 +in
    1.82 +
    1.83  fun read init master_dir blobs span =
    1.84    let
    1.85      val outer_syntax = #2 (Outer_Syntax.get_syntax ());
    1.86 @@ -149,6 +162,8 @@
    1.87        handle ERROR msg => Toplevel.malformed (#1 proper_range) msg
    1.88    end;
    1.89  
    1.90 +end;
    1.91 +
    1.92  
    1.93  (* eval *)
    1.94