simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
authorwenzelm
Mon Apr 07 23:02:29 2014 +0200 (2014-04-07)
changeset 56458a8d960baa5c2
parent 56457 eea4bbe15745
child 56459 38d0b2099743
simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
more liberal hyperlink to files, allow hyperlinks within editor files independently of the (POSIX) file-system;
src/Pure/PIDE/command.ML
src/Pure/PIDE/document.ML
src/Pure/PIDE/protocol.ML
src/Pure/PIDE/protocol.scala
src/Tools/jEdit/src/jedit_editor.scala
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Pure/PIDE/command.ML	Mon Apr 07 21:23:02 2014 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Mon Apr 07 23:02:29 2014 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  signature COMMAND =
     1.6  sig
     1.7 -  type blob = (string * string * (SHA1.digest * string list) option) Exn.result
     1.8 +  type blob = (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 * string * (SHA1.digest * string list) option) Exn.result;  (*file, path, digest, lines*)
    1.17 +  (string * (SHA1.digest * string list) option) Exn.result;  (*file node name, digest, lines*)
    1.18  
    1.19  fun read_file master_dir pos src_path =
    1.20    let
    1.21 @@ -115,16 +115,16 @@
    1.22      [span] => span
    1.23        |> Thy_Syntax.resolve_files (fn cmd => fn (path, pos) =>
    1.24          let
    1.25 -          fun make_file src_path (Exn.Res (_, _, NONE)) =
    1.26 +          fun make_file src_path (Exn.Res (_, NONE)) =
    1.27                  Exn.interruptible_capture (fn () => read_file master_dir pos src_path) ()
    1.28 -            | make_file src_path (Exn.Res (file_node, file_path, SOME (digest, lines))) =
    1.29 -               (Position.reports [(pos, Markup.language_path), (pos, Markup.path file_path)];
    1.30 +            | make_file src_path (Exn.Res (file_node, SOME (digest, lines))) =
    1.31 +               (Position.reports [(pos, Markup.language_path), (pos, Markup.path file_node)];
    1.32                  Exn.Res (blob_file src_path lines digest file_node))
    1.33              | make_file _ (Exn.Exn e) = Exn.Exn e;
    1.34            val src_paths = Keyword.command_files cmd path;
    1.35          in
    1.36            if null blobs then
    1.37 -            map2 make_file src_paths (map (K (Exn.Res ("", "", NONE))) src_paths)
    1.38 +            map2 make_file src_paths (map (K (Exn.Res ("", NONE))) src_paths)
    1.39            else if length src_paths = length blobs then
    1.40              map2 make_file src_paths blobs
    1.41            else error ("Misalignment of inlined files" ^ Position.here pos)
     2.1 --- a/src/Pure/PIDE/document.ML	Mon Apr 07 21:23:02 2014 +0200
     2.2 +++ b/src/Pure/PIDE/document.ML	Mon Apr 07 23:02:29 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 * string option) Exn.result
     2.8 +  type blob_digest = (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,8 +219,7 @@
    2.13  
    2.14  (** main state -- document structure and execution process **)
    2.15  
    2.16 -type blob_digest =
    2.17 -  (string * string * string option) Exn.result;  (* file node name, path, raw digest*)
    2.18 +type blob_digest = (string * string option) Exn.result;  (*file node name, raw digest*)
    2.19  
    2.20  type execution =
    2.21   {version_id: Document_ID.version,  (*static version id*)
    2.22 @@ -293,8 +292,8 @@
    2.23    | SOME content => content);
    2.24  
    2.25  fun resolve_blob state (blob_digest: blob_digest) =
    2.26 -  blob_digest |> Exn.map_result (fn (file, path, raw_digest) =>
    2.27 -    (file, path, Option.map (the_blob state) raw_digest));
    2.28 +  blob_digest |> Exn.map_result (fn (file_node, raw_digest) =>
    2.29 +    (file_node, Option.map (the_blob state) raw_digest));
    2.30  
    2.31  
    2.32  (* commands *)
    2.33 @@ -343,7 +342,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  
     3.1 --- a/src/Pure/PIDE/protocol.ML	Mon Apr 07 21:23:02 2014 +0200
     3.2 +++ b/src/Pure/PIDE/protocol.ML	Mon Apr 07 23:02:29 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 (triple string string (option string) a),
     3.8 +               [fn ([], a) => Exn.Res (pair 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	Mon Apr 07 21:23:02 2014 +0200
     4.2 +++ b/src/Pure/PIDE/protocol.scala	Mon Apr 07 23:02:29 2014 +0200
     4.3 @@ -352,8 +352,7 @@
     4.4        val encode_blob: T[Command.Blob] =
     4.5          variant(List(
     4.6            { case Exn.Res((a, b)) =>
     4.7 -              (Nil, triple(string, string, option(string))(
     4.8 -                (a.node, Isabelle_System.posix_path_url(a.node), b.map(p => p._1.toString)))) },
     4.9 +              (Nil, pair(string, option(string))((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      }
     5.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Apr 07 21:23:02 2014 +0200
     5.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Apr 07 23:02:29 2014 +0200
     5.3 @@ -195,26 +195,32 @@
     5.4    def hyperlink_source_file(source_name: String, line: Int, offset: Symbol.Offset)
     5.5      : Option[Hyperlink] =
     5.6    {
     5.7 -    if (Path.is_valid(source_name)) {
     5.8 -      Isabelle_System.source_file(Path.explode(source_name)) match {
     5.9 -        case Some(path) =>
    5.10 -          val name = Isabelle_System.platform_path(path)
    5.11 -          JEdit_Lib.jedit_buffer(name) match {
    5.12 -            case Some(buffer) if offset > 0 =>
    5.13 -              val (line, column) =
    5.14 -                JEdit_Lib.buffer_lock(buffer) {
    5.15 -                  ((1, 1) /:
    5.16 -                    (Symbol.iterator(JEdit_Lib.buffer_text(buffer)).
    5.17 -                      zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(
    5.18 -                        Symbol.advance_line_column)
    5.19 -                }
    5.20 -              Some(hyperlink_file(name, line, column))
    5.21 -            case _ => Some(hyperlink_file(name, line))
    5.22 -          }
    5.23 -        case None => None
    5.24 +    val opt_name =
    5.25 +      if (Path.is_wellformed(source_name)) {
    5.26 +        if (Path.is_valid(source_name)) {
    5.27 +          val path = Path.explode(source_name)
    5.28 +          Some(Isabelle_System.platform_path(Isabelle_System.source_file(path) getOrElse path))
    5.29 +        }
    5.30 +        else None
    5.31        }
    5.32 +      else Some(source_name)
    5.33 +
    5.34 +    opt_name match {
    5.35 +      case Some(name) =>
    5.36 +        JEdit_Lib.jedit_buffer(name) match {
    5.37 +          case Some(buffer) if offset > 0 =>
    5.38 +            val (line, column) =
    5.39 +              JEdit_Lib.buffer_lock(buffer) {
    5.40 +                ((1, 1) /:
    5.41 +                  (Symbol.iterator(JEdit_Lib.buffer_text(buffer)).
    5.42 +                    zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(
    5.43 +                      Symbol.advance_line_column)
    5.44 +              }
    5.45 +            Some(hyperlink_file(name, line, column))
    5.46 +          case _ => Some(hyperlink_file(name, line))
    5.47 +        }
    5.48 +      case None => None
    5.49      }
    5.50 -    else None
    5.51    }
    5.52  
    5.53    def hyperlink_url(name: String): Hyperlink =
     6.1 --- a/src/Tools/jEdit/src/rendering.scala	Mon Apr 07 21:23:02 2014 +0200
     6.2 +++ b/src/Tools/jEdit/src/rendering.scala	Mon Apr 07 23:02:29 2014 +0200
     6.3 @@ -321,15 +321,18 @@
     6.4  
     6.5    /* hyperlinks */
     6.6  
     6.7 +  private def jedit_file(name: String): String =
     6.8 +    if (Path.is_valid(name))
     6.9 +      PIDE.resources.append(snapshot.node_name.master_dir, Path.explode(name))
    6.10 +    else name
    6.11 +
    6.12    def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
    6.13    {
    6.14      snapshot.cumulate[Vector[Text.Info[PIDE.editor.Hyperlink]]](
    6.15        range, Vector.empty, Rendering.hyperlink_elements, _ =>
    6.16          {
    6.17 -          case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _)))
    6.18 -          if Path.is_valid(name) =>
    6.19 -            val jedit_file = PIDE.resources.append(snapshot.node_name.master_dir, Path.explode(name))
    6.20 -            val link = PIDE.editor.hyperlink_file(jedit_file)
    6.21 +          case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _))) =>
    6.22 +            val link = PIDE.editor.hyperlink_file(jedit_file(name))
    6.23              Some(links :+ Text.Info(snapshot.convert(info_range), link))
    6.24  
    6.25            case (links, Text.Info(info_range, XML.Elem(Markup.Url(name), _))) =>
    6.26 @@ -457,10 +460,11 @@
    6.27                  "\n" + t.message
    6.28                else ""
    6.29              Some(add(prev, r, (true, XML.Text(txt1 + txt2))))
    6.30 -          case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _)))
    6.31 -          if Path.is_valid(name) =>
    6.32 -            val jedit_file = PIDE.resources.append(snapshot.node_name.master_dir, Path.explode(name))
    6.33 -            val text = "path " + quote(name) + "\nfile " + quote(jedit_file)
    6.34 +          case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _))) =>
    6.35 +            val file = jedit_file(name)
    6.36 +            val text =
    6.37 +              if (name == file) "file " + quote(file)
    6.38 +              else "path " + quote(name) + "\nfile " + quote(file)
    6.39              Some(add(prev, r, (true, XML.Text(text))))
    6.40            case (prev, Text.Info(r, XML.Elem(Markup.Url(name), _))) =>
    6.41              Some(add(prev, r, (true, XML.Text("URL " + quote(name)))))