separate file_node vs. file_path, e.g. relevant on Windows for hyperlink to the latter;
authorwenzelm
Mon Apr 07 13:06:34 2014 +0200 (2014-04-07)
changeset 564471e77ed11f2f7
parent 56446 70a13de8a154
child 56448 344800503974
separate file_node vs. file_path, e.g. relevant on Windows for hyperlink to the latter;
src/Pure/PIDE/command.ML
src/Pure/PIDE/document.ML
src/Pure/PIDE/protocol.ML
src/Pure/PIDE/protocol.scala
     1.1 --- a/src/Pure/PIDE/command.ML	Sun Apr 06 21:01:45 2014 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Mon Apr 07 13:06:34 2014 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  signature COMMAND =
     1.6  sig
     1.7 -  type blob = (string * (SHA1.digest * string list) option) Exn.result
     1.8 +  type blob = (string * string * (SHA1.digest * string list) option) Exn.result
     1.9    val read_file: Path.T -> Position.T -> Path.T -> Token.file
    1.10    val read: (unit -> theory) -> Path.T -> blob list -> Token.T list -> Toplevel.transition
    1.11    type eval
    1.12 @@ -87,7 +87,7 @@
    1.13  (* read *)
    1.14  
    1.15  type blob =
    1.16 -  (string * (SHA1.digest * string list) option) Exn.result;  (*file node name, digest, lines*)
    1.17 +  (string * string * (SHA1.digest * string list) option) Exn.result;  (*file, path, digest, lines*)
    1.18  
    1.19  fun read_file master_dir pos src_path =
    1.20    let
    1.21 @@ -101,10 +101,10 @@
    1.22  
    1.23  local
    1.24  
    1.25 -fun blob_file src_path lines digest file =
    1.26 +fun blob_file src_path lines digest file_node =
    1.27    let
    1.28      val file_pos =
    1.29 -      Position.file file (*sic!*) |>
    1.30 +      Position.file file_node |>
    1.31        (case Position.get_id (Position.thread_data ()) of
    1.32          NONE => I
    1.33        | SOME exec_id => Position.put_id exec_id);
    1.34 @@ -115,16 +115,16 @@
    1.35      [span] => span
    1.36        |> Thy_Syntax.resolve_files (fn cmd => fn (path, pos) =>
    1.37          let
    1.38 -          fun make_file src_path (Exn.Res (_, NONE)) =
    1.39 +          fun make_file src_path (Exn.Res (_, _, NONE)) =
    1.40                  Exn.interruptible_capture (fn () => read_file master_dir pos src_path) ()
    1.41 -            | make_file src_path (Exn.Res (file, SOME (digest, lines))) =
    1.42 -               (Position.reports [(pos, Markup.language_path), (pos, Markup.path file)];
    1.43 -                Exn.Res (blob_file src_path lines digest file))
    1.44 +            | make_file src_path (Exn.Res (file_node, file_path, SOME (digest, lines))) =
    1.45 +               (Position.reports [(pos, Markup.language_path), (pos, Markup.path file_path)];
    1.46 +                Exn.Res (blob_file src_path lines digest file_node))
    1.47              | make_file _ (Exn.Exn e) = Exn.Exn e;
    1.48            val src_paths = Keyword.command_files cmd path;
    1.49          in
    1.50            if null blobs then
    1.51 -            map2 make_file src_paths (map (K (Exn.Res ("", NONE))) src_paths)
    1.52 +            map2 make_file src_paths (map (K (Exn.Res ("", "", NONE))) src_paths)
    1.53            else if length src_paths = length blobs then
    1.54              map2 make_file src_paths blobs
    1.55            else error ("Misalignment of inlined files" ^ Position.here pos)
     2.1 --- a/src/Pure/PIDE/document.ML	Sun Apr 06 21:01:45 2014 +0200
     2.2 +++ b/src/Pure/PIDE/document.ML	Mon Apr 07 13:06:34 2014 +0200
     2.3 @@ -18,7 +18,7 @@
     2.4    type state
     2.5    val init_state: state
     2.6    val define_blob: string -> string -> state -> state
     2.7 -  type blob_digest = (string * string option) Exn.result
     2.8 +  type blob_digest = (string * string * string option) Exn.result
     2.9    val define_command: Document_ID.command -> string -> blob_digest list -> string ->
    2.10      state -> state
    2.11    val remove_versions: Document_ID.version list -> state -> state
    2.12 @@ -219,7 +219,8 @@
    2.13  
    2.14  (** main state -- document structure and execution process **)
    2.15  
    2.16 -type blob_digest = (string * string option) Exn.result;  (* file node name, raw digest*)
    2.17 +type blob_digest =
    2.18 +  (string * string * string option) Exn.result;  (* file node name, path, raw digest*)
    2.19  
    2.20  type execution =
    2.21   {version_id: Document_ID.version,  (*static version id*)
    2.22 @@ -291,6 +292,10 @@
    2.23      NONE => error ("Undefined blob: " ^ digest)
    2.24    | SOME content => content);
    2.25  
    2.26 +fun resolve_blob state (blob_digest: blob_digest) =
    2.27 +  blob_digest |> Exn.map_result (fn (file, path, raw_digest) =>
    2.28 +    (file, path, Option.map (the_blob state) raw_digest));
    2.29 +
    2.30  
    2.31  (* commands *)
    2.32  
    2.33 @@ -338,7 +343,7 @@
    2.34      val blobs' =
    2.35        (commands', Symtab.empty) |->
    2.36          Inttab.fold (fn (_, (_, blobs, _)) => blobs |>
    2.37 -          fold (fn Exn.Res (_, SOME b) => Symtab.update (b, the_blob state b) | _ => I));
    2.38 +          fold (fn Exn.Res (_, _, SOME b) => Symtab.update (b, the_blob state b) | _ => I));
    2.39  
    2.40    in (versions', blobs', commands', execution) end);
    2.41  
    2.42 @@ -505,7 +510,7 @@
    2.43        val command_visible = visible_command node command_id';
    2.44        val command_overlays = overlays node command_id';
    2.45        val (command_name, blob_digests, span0) = the_command state command_id';
    2.46 -      val blobs = (map o Exn.map_result o apsnd o Option.map) (the_blob state) blob_digests;
    2.47 +      val blobs = map (resolve_blob state) blob_digests;
    2.48        val span = Lazy.force span0;
    2.49  
    2.50        val eval' =
     3.1 --- a/src/Pure/PIDE/protocol.ML	Sun Apr 06 21:01:45 2014 +0200
     3.2 +++ b/src/Pure/PIDE/protocol.ML	Mon Apr 07 13:06:34 2014 +0200
     3.3 @@ -34,7 +34,7 @@
     3.4            YXML.parse_body blobs_yxml |>
     3.5              let open XML.Decode in
     3.6                list (variant
     3.7 -               [fn ([], a) => Exn.Res (pair string (option string) a),
     3.8 +               [fn ([], a) => Exn.Res (triple string string (option string) a),
     3.9                  fn ([], a) => Exn.Exn (ERROR (string a))])
    3.10              end;
    3.11        in
     4.1 --- a/src/Pure/PIDE/protocol.scala	Sun Apr 06 21:01:45 2014 +0200
     4.2 +++ b/src/Pure/PIDE/protocol.scala	Mon Apr 07 13:06:34 2014 +0200
     4.3 @@ -352,7 +352,8 @@
     4.4        val encode_blob: T[Command.Blob] =
     4.5          variant(List(
     4.6            { case Exn.Res((a, b)) =>
     4.7 -              (Nil, pair(string, option(string))((a.node, b.map(p => p._1.toString)))) },
     4.8 +              (Nil, triple(string, string, option(string))(
     4.9 +                (a.node, Isabelle_System.posix_path(a.node), b.map(p => p._1.toString)))) },
    4.10            { case Exn.Exn(e) => (Nil, string(Exn.message(e))) }))
    4.11        YXML.string_of_body(list(encode_blob)(command.blobs))
    4.12      }