merged
authorwenzelm
Fri Aug 12 23:29:28 2011 +0200 (2011-08-12)
changeset 4417221f97048b478
parent 44171 75ea0e390a92
parent 44163 32e0c150c010
child 44173 aaaa13e297dc
merged
     1.1 --- a/src/Pure/General/exn.ML	Fri Aug 12 09:17:30 2011 -0700
     1.2 +++ b/src/Pure/General/exn.ML	Fri Aug 12 23:29:28 2011 +0200
     1.3 @@ -30,7 +30,7 @@
     1.4  structure Exn: EXN =
     1.5  struct
     1.6  
     1.7 -(* runtime exceptions as values *)
     1.8 +(* exceptions as values *)
     1.9  
    1.10  datatype 'a result =
    1.11    Res of 'a |
     2.1 --- a/src/Pure/General/exn.scala	Fri Aug 12 09:17:30 2011 -0700
     2.2 +++ b/src/Pure/General/exn.scala	Fri Aug 12 23:29:28 2011 +0200
     2.3 @@ -9,7 +9,7 @@
     2.4  
     2.5  object Exn
     2.6  {
     2.7 -  /* runtime exceptions as values */
     2.8 +  /* exceptions as values */
     2.9  
    2.10    sealed abstract class Result[A]
    2.11    case class Res[A](res: A) extends Result[A]
    2.12 @@ -24,5 +24,17 @@
    2.13        case Res(x) => x
    2.14        case Exn(exn) => throw exn
    2.15      }
    2.16 +
    2.17 +
    2.18 +  /* message */
    2.19 +
    2.20 +  private val runtime_exception = Class.forName("java.lang.RuntimeException")
    2.21 +
    2.22 +  def message(exn: Throwable): String =
    2.23 +    if (exn.getClass == runtime_exception) {
    2.24 +      val msg = exn.getMessage
    2.25 +      if (msg == null) "Error" else msg
    2.26 +    }
    2.27 +    else exn.toString
    2.28  }
    2.29  
     3.1 --- a/src/Pure/General/graph.ML	Fri Aug 12 09:17:30 2011 -0700
     3.2 +++ b/src/Pure/General/graph.ML	Fri Aug 12 23:29:28 2011 +0200
     3.3 @@ -49,6 +49,8 @@
     3.4    val topological_order: 'a T -> key list
     3.5    val add_edge_trans_acyclic: key * key -> 'a T -> 'a T               (*exception CYCLES*)
     3.6    val merge_trans_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T   (*exception CYCLES*)
     3.7 +  exception DEP of key * key
     3.8 +  val schedule: ((key * 'b) list -> key * 'a -> 'b) -> 'a T -> 'b list  (*exception DEP*)
     3.9  end;
    3.10  
    3.11  functor Graph(Key: KEY): GRAPH =
    3.12 @@ -285,6 +287,24 @@
    3.13      |> fold add_edge_trans_acyclic (diff_edges G2 G1);
    3.14  
    3.15  
    3.16 +(* schedule acyclic graph *)
    3.17 +
    3.18 +exception DEP of key * key;
    3.19 +
    3.20 +fun schedule f G =
    3.21 +  let
    3.22 +    val xs = topological_order G;
    3.23 +    val results = (xs, Table.empty) |-> fold (fn x => fn tab =>
    3.24 +      let
    3.25 +        val a = get_node G x;
    3.26 +        val deps = imm_preds G x |> map (fn y =>
    3.27 +          (case Table.lookup tab y of
    3.28 +            SOME b => (y, b)
    3.29 +          | NONE => raise DEP (x, y)));
    3.30 +      in Table.update (x, f deps (x, a)) tab end);
    3.31 +  in map (the o Table.lookup results) xs end;
    3.32 +
    3.33 +
    3.34  (*final declarations of this structure!*)
    3.35  val map = map_nodes;
    3.36  val fold = fold_graph;
     4.1 --- a/src/Pure/General/path.ML	Fri Aug 12 09:17:30 2011 -0700
     4.2 +++ b/src/Pure/General/path.ML	Fri Aug 12 23:29:28 2011 +0200
     4.3 @@ -51,7 +51,7 @@
     4.4    | check_elem (chs as ["~"]) = err_elem "Illegal" chs
     4.5    | check_elem (chs as ["~", "~"]) = err_elem "Illegal" chs
     4.6    | check_elem chs =
     4.7 -      (case inter (op =) ["/", "\\", "$", ":"] chs of
     4.8 +      (case inter (op =) ["/", "\\", ":"] chs of
     4.9          [] => chs
    4.10        | bads => err_elem ("Illegal character(s) " ^ commas_quote bads ^ " in") chs);
    4.11  
     5.1 --- a/src/Pure/PIDE/document.ML	Fri Aug 12 09:17:30 2011 -0700
     5.2 +++ b/src/Pure/PIDE/document.ML	Fri Aug 12 23:29:28 2011 +0200
     5.3 @@ -249,14 +249,13 @@
     5.4  
     5.5  in
     5.6  
     5.7 -fun run_command thy_name raw_tr st =
     5.8 +fun run_command node_name raw_tr st =
     5.9    (case
    5.10        (case Toplevel.init_of raw_tr of
    5.11 -        SOME name => Exn.capture (fn () =>
    5.12 -          let
    5.13 -            val path = Path.explode thy_name;
    5.14 -            val _ = Thy_Header.consistent_name (Path.implode (Path.base path)) name;
    5.15 -          in Toplevel.modify_master (SOME (Path.dir path)) raw_tr end) ()
    5.16 +        SOME name =>
    5.17 +          Exn.capture (fn () =>
    5.18 +            let val master_dir = Path.dir (Path.explode node_name);  (* FIXME move to Scala side *)
    5.19 +            in Toplevel.modify_master (SOME master_dir) raw_tr end) ()
    5.20        | NONE => Exn.Res raw_tr) of
    5.21      Exn.Res tr =>
    5.22        let
     6.1 --- a/src/Pure/PIDE/document.scala	Fri Aug 12 09:17:30 2011 -0700
     6.2 +++ b/src/Pure/PIDE/document.scala	Fri Aug 12 23:29:28 2011 +0200
     6.3 @@ -51,8 +51,17 @@
     6.4      case class Edits[A](edits: List[A]) extends Edit[A]
     6.5      case class Update_Header[A](header: Header) extends Edit[A]
     6.6  
     6.7 -    sealed case class Header(val master_dir: Path, val thy_header: Exn.Result[Thy_Header.Header])
     6.8 -    val empty_header = Header(Path.current, Exn.Exn(ERROR("Bad theory header")))
     6.9 +    sealed case class Header(val master_dir: String, val thy_header: Exn.Result[Thy_Header])
    6.10 +    {
    6.11 +      def norm_deps(f: (String, Path) => String): Header =
    6.12 +        copy(thy_header =
    6.13 +          thy_header match {
    6.14 +            case Exn.Res(header) =>
    6.15 +              Exn.capture { header.norm_deps(name => f(master_dir, Path.explode(name))) }
    6.16 +            case exn => exn
    6.17 +          })
    6.18 +    }
    6.19 +    val empty_header = Header("", Exn.Exn(ERROR("Bad theory header")))
    6.20  
    6.21      val empty: Node = Node(empty_header, Map(), Linear_Set())
    6.22  
     7.1 --- a/src/Pure/PIDE/isar_document.scala	Fri Aug 12 09:17:30 2011 -0700
     7.2 +++ b/src/Pure/PIDE/isar_document.scala	Fri Aug 12 23:29:28 2011 +0200
     7.3 @@ -150,10 +150,10 @@
     7.4              { case Document.Node.Remove() => (Nil, Nil) },
     7.5              { case Document.Node.Edits(a) => (Nil, list(pair(option(long), option(long)))(a)) },
     7.6              { case Document.Node.Update_Header(
     7.7 -                  Document.Node.Header(_, Exn.Res(Thy_Header.Header(a, b, c)))) =>
     7.8 +                  Document.Node.Header(_, Exn.Res(Thy_Header(a, b, c)))) =>
     7.9                  (Nil, triple(string, list(string), list(string))(a, b, c)) },
    7.10              { case Document.Node.Update_Header(
    7.11 -                  Document.Node.Header(_, Exn.Exn(ERROR(a)))) => (List(a), Nil) }))))
    7.12 +                  Document.Node.Header(_, Exn.Exn(e))) => (List(Exn.message(e)), Nil) }))))
    7.13        YXML.string_of_body(encode(edits)) }
    7.14  
    7.15      input("Isar_Document.edit_version", Document.ID(old_id), Document.ID(new_id), edits_yxml)
     8.1 --- a/src/Pure/System/invoke_scala.scala	Fri Aug 12 09:17:30 2011 -0700
     8.2 +++ b/src/Pure/System/invoke_scala.scala	Fri Aug 12 23:29:28 2011 +0200
     8.3 @@ -57,10 +57,8 @@
     8.4          Exn.capture { f(arg) } match {
     8.5            case Exn.Res(null) => (Tag.NULL, "")
     8.6            case Exn.Res(res) => (Tag.OK, res)
     8.7 -          case Exn.Exn(ERROR(msg)) => (Tag.ERROR, msg)
     8.8 -          case Exn.Exn(e) => (Tag.ERROR, e.toString)
     8.9 +          case Exn.Exn(e) => (Tag.ERROR, Exn.message(e))
    8.10          }
    8.11 -      case Exn.Exn(ERROR(msg)) => (Tag.FAIL, msg)
    8.12 -      case Exn.Exn(e) => (Tag.FAIL, e.toString)
    8.13 +      case Exn.Exn(e) => (Tag.FAIL, Exn.message(e))
    8.14      }
    8.15  }
     9.1 --- a/src/Pure/System/session.scala	Fri Aug 12 09:17:30 2011 -0700
     9.2 +++ b/src/Pure/System/session.scala	Fri Aug 12 23:29:28 2011 +0200
     9.3 @@ -20,7 +20,8 @@
     9.4  
     9.5    abstract class File_Store
     9.6    {
     9.7 -    def read(path: Path): String
     9.8 +    def append(master_dir: String, path: Path): String
     9.9 +    def require(file: String): Unit
    9.10    }
    9.11  
    9.12  
    9.13 @@ -146,7 +147,7 @@
    9.14      override def is_loaded(name: String): Boolean =
    9.15        loaded_theories.contains(name)
    9.16  
    9.17 -    override def check_thy(dir: Path, name: String): (String, Thy_Header.Header) =
    9.18 +    override def check_thy(dir: Path, name: String): (String, Thy_Header) =
    9.19      {
    9.20        val file = Isabelle_System.platform_file(dir + Thy_Header.thy_path(name))
    9.21        if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
    9.22 @@ -186,7 +187,8 @@
    9.23        val syntax = current_syntax()
    9.24        val previous = global_state().history.tip.version
    9.25        val doc_edits =
    9.26 -        (name, Document.Node.Update_Header[Text.Edit](header)) :: edits.map(edit => (name, edit))
    9.27 +        (name, Document.Node.Update_Header[Text.Edit](header.norm_deps(file_store.append))) ::
    9.28 +          edits.map(edit => (name, edit))
    9.29        val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, doc_edits) }
    9.30        val change =
    9.31          global_state.change_yield(_.extend_history(previous, doc_edits, result.map(_._2)))
    10.1 --- a/src/Pure/Thy/thy_header.ML	Fri Aug 12 09:17:30 2011 -0700
    10.2 +++ b/src/Pure/Thy/thy_header.ML	Fri Aug 12 23:29:28 2011 +0200
    10.3 @@ -9,7 +9,6 @@
    10.4    val args: Token.T list -> (string * string list * (string * bool) list) * Token.T list
    10.5    val read: Position.T -> string -> string * string list * (Path.T * bool) list
    10.6    val thy_path: string -> Path.T
    10.7 -  val split_thy_path: Path.T -> Path.T * string
    10.8    val consistent_name: string -> string -> unit
    10.9  end;
   10.10  
   10.11 @@ -73,11 +72,6 @@
   10.12  
   10.13  val thy_path = Path.ext "thy" o Path.basic;
   10.14  
   10.15 -fun split_thy_path path =
   10.16 -  (case Path.split_ext path of
   10.17 -    (path', "thy") => (Path.dir path', Path.implode (Path.base path'))
   10.18 -  | _ => error ("Bad theory file specification: " ^ Path.print path));
   10.19 -
   10.20  fun consistent_name name name' =
   10.21    if name = name' then ()
   10.22    else error ("Bad file name " ^ Path.print (thy_path name) ^ " for theory " ^ quote name');
    11.1 --- a/src/Pure/Thy/thy_header.scala	Fri Aug 12 09:17:30 2011 -0700
    11.2 +++ b/src/Pure/Thy/thy_header.scala	Fri Aug 12 23:29:28 2011 +0200
    11.3 @@ -25,27 +25,20 @@
    11.4  
    11.5    val lexicon = Scan.Lexicon("%", "(", ")", ";", BEGIN, HEADER, IMPORTS, THEORY, USES)
    11.6  
    11.7 -  sealed case class Header(val name: String, val imports: List[String], val uses: List[String])
    11.8 -  {
    11.9 -    def map(f: String => String): Header =
   11.10 -      Header(f(name), imports.map(f), uses.map(f))
   11.11 -  }
   11.12 +
   11.13 +  /* theory file name */
   11.14  
   11.15 +  private val Thy_Name = new Regex(""".*?([^/\\:]+)\.thy""")
   11.16  
   11.17 -  /* file name */
   11.18 +  def thy_name(s: String): Option[String] =
   11.19 +    s match { case Thy_Name(name) => Some(name) case _ => None }
   11.20  
   11.21    def thy_path(name: String): Path = Path.basic(name).ext("thy")
   11.22  
   11.23 -  def split_thy_path(path: Path): (Path, String) =
   11.24 -    path.split_ext match {
   11.25 -      case (path1, "thy") => (path1.dir, path1.base.implode)
   11.26 -      case _ => error("Bad theory file specification: " + path)
   11.27 -    }
   11.28 -
   11.29  
   11.30    /* header */
   11.31  
   11.32 -  val header: Parser[Header] =
   11.33 +  val header: Parser[Thy_Header] =
   11.34    {
   11.35      val file_name = atom("file name", _.is_name)
   11.36      val theory_name = atom("theory name", _.is_name)
   11.37 @@ -57,7 +50,7 @@
   11.38  
   11.39      val args =
   11.40        theory_name ~ (keyword(IMPORTS) ~! (rep1(theory_name) ~ uses ~ keyword(BEGIN))) ^^
   11.41 -        { case x ~ (_ ~ (ys ~ zs ~ _)) => Header(x, ys, zs) }
   11.42 +        { case x ~ (_ ~ (ys ~ zs ~ _)) => Thy_Header(x, ys, zs) }
   11.43  
   11.44      (keyword(HEADER) ~ tags) ~!
   11.45        ((doc_source ~ rep(keyword(";")) ~ keyword(THEORY) ~ tags) ~> args) ^^ { case _ ~ x => x } |
   11.46 @@ -67,7 +60,7 @@
   11.47  
   11.48    /* read -- lazy scanning */
   11.49  
   11.50 -  def read(reader: Reader[Char]): Header =
   11.51 +  def read(reader: Reader[Char]): Thy_Header =
   11.52    {
   11.53      val token = lexicon.token(_ => false)
   11.54      val toks = new mutable.ListBuffer[Token]
   11.55 @@ -89,10 +82,10 @@
   11.56      }
   11.57    }
   11.58  
   11.59 -  def read(source: CharSequence): Header =
   11.60 +  def read(source: CharSequence): Thy_Header =
   11.61      read(new CharSequenceReader(source))
   11.62  
   11.63 -  def read(file: File): Header =
   11.64 +  def read(file: File): Thy_Header =
   11.65    {
   11.66      val reader = Scan.byte_reader(file)
   11.67      try { read(reader).map(Standard_System.decode_permissive_utf8) }
   11.68 @@ -102,7 +95,7 @@
   11.69  
   11.70    /* check */
   11.71  
   11.72 -  def check(name: String, source: CharSequence): Header =
   11.73 +  def check(name: String, source: CharSequence): Thy_Header =
   11.74    {
   11.75      val header = read(source)
   11.76      val name1 = header.name
   11.77 @@ -111,3 +104,14 @@
   11.78      header
   11.79    }
   11.80  }
   11.81 +
   11.82 +
   11.83 +sealed case class Thy_Header(val name: String, val imports: List[String], val uses: List[String])
   11.84 +{
   11.85 +  def map(f: String => String): Thy_Header =
   11.86 +    Thy_Header(f(name), imports.map(f), uses.map(f))
   11.87 +
   11.88 +  def norm_deps(f: String => String): Thy_Header =
   11.89 +    copy(imports = imports.map(name => f(name) + ".thy"), uses = uses.map(f))
   11.90 +}
   11.91 +
    12.1 --- a/src/Pure/Thy/thy_info.ML	Fri Aug 12 09:17:30 2011 -0700
    12.2 +++ b/src/Pure/Thy/thy_info.ML	Fri Aug 12 23:29:28 2011 +0200
    12.3 @@ -178,51 +178,37 @@
    12.4  fun task_finished (Task _) = false
    12.5    | task_finished (Finished _) = true;
    12.6  
    12.7 +fun task_parents deps (parents: string list) = map (the o AList.lookup (op =) deps) parents;
    12.8 +
    12.9  local
   12.10  
   12.11  fun finish_thy ((thy, present, commit): result) =
   12.12    (Global_Theory.join_proofs thy; Future.join present; commit (); thy);
   12.13  
   12.14 -fun schedule_seq task_graph =
   12.15 -  ((Graph.topological_order task_graph, Symtab.empty) |-> fold (fn name => fn tab =>
   12.16 -    (case Graph.get_node task_graph name of
   12.17 -      Task (parents, body) =>
   12.18 -        let val result = body (map (the o Symtab.lookup tab) parents)
   12.19 -        in Symtab.update (name, finish_thy result) tab end
   12.20 -    | Finished thy => Symtab.update (name, thy) tab))) |> ignore;
   12.21 -
   12.22 -fun schedule_futures task_graph = uninterruptible (fn _ => fn () =>
   12.23 -  let
   12.24 -    val tasks = Graph.topological_order task_graph;
   12.25 -    val futures = (tasks, Symtab.empty) |-> fold (fn name => fn tab =>
   12.26 -      (case Graph.get_node task_graph name of
   12.27 -        Task (parents, body) =>
   12.28 -          let
   12.29 -            val get = the o Symtab.lookup tab;
   12.30 -            val deps = map (`get) (Graph.imm_preds task_graph name);
   12.31 -            val task_deps = map (Future.task_of o #1) deps;
   12.32 -            fun failed (future, parent) = if can Future.join future then NONE else SOME parent;
   12.33 +val schedule_seq =
   12.34 +  Graph.schedule (fn deps => fn (_, task) =>
   12.35 +    (case task of
   12.36 +      Task (parents, body) => finish_thy (body (task_parents deps parents))
   12.37 +    | Finished thy => thy)) #> ignore;
   12.38  
   12.39 -            val future =
   12.40 -              singleton
   12.41 -                (Future.forks
   12.42 -                  {name = "theory:" ^ name, group = NONE, deps = task_deps, pri = 0,
   12.43 -                    interrupts = true})
   12.44 -                (fn () =>
   12.45 -                  (case map_filter failed deps of
   12.46 -                    [] => body (map (#1 o Future.join o get) parents)
   12.47 -                  | bad => error (loader_msg ("failed to load " ^ quote name ^
   12.48 -                      " (unresolved " ^ commas_quote bad ^ ")") [])));
   12.49 -          in Symtab.update (name, future) tab end
   12.50 -      | Finished thy => Symtab.update (name, Future.value (thy, Future.value (), I)) tab));
   12.51 -    val _ =
   12.52 -      tasks |> maps (fn name =>
   12.53 -        let
   12.54 -          val result = Future.join (the (Symtab.lookup futures name));
   12.55 -          val _ = finish_thy result;
   12.56 -        in [] end handle exn => [Exn.Exn exn])
   12.57 -      |> rev |> Exn.release_all;
   12.58 -  in () end) ();
   12.59 +val schedule_futures = uninterruptible (fn _ =>
   12.60 +  Graph.schedule (fn deps => fn (name, task) =>
   12.61 +    (case task of
   12.62 +      Task (parents, body) =>
   12.63 +        singleton
   12.64 +          (Future.forks
   12.65 +            {name = "theory:" ^ name, group = NONE,
   12.66 +              deps = map (Future.task_of o #2) deps,
   12.67 +              pri = 0, interrupts = true})
   12.68 +          (fn () =>
   12.69 +            (case filter (not o can Future.join o #2) deps of
   12.70 +              [] => body (map (#1 o Future.join) (task_parents deps parents))
   12.71 +            | bad =>
   12.72 +                error (loader_msg ("failed to load " ^ quote name ^
   12.73 +                  " (unresolved " ^ commas_quote (map #1 bad) ^ ")") [])))
   12.74 +    | Finished thy => Future.value (thy, Future.value (), I)))
   12.75 +  #> maps (fn result => (finish_thy (Future.join result); []) handle exn => [Exn.Exn exn])
   12.76 +  #> rev #> Exn.release_all) #> ignore;
   12.77  
   12.78  in
   12.79  
    13.1 --- a/src/Pure/Thy/thy_info.scala	Fri Aug 12 09:17:30 2011 -0700
    13.2 +++ b/src/Pure/Thy/thy_info.scala	Fri Aug 12 23:29:28 2011 +0200
    13.3 @@ -38,7 +38,7 @@
    13.4  
    13.5    /* dependencies */
    13.6  
    13.7 -  type Deps = Map[String, Exn.Result[(String, Thy_Header.Header)]]  // name -> (text, header)
    13.8 +  type Deps = Map[String, Exn.Result[(String, Thy_Header)]]  // name -> (text, header)
    13.9  
   13.10    private def require_thys(ignored: String => Boolean,
   13.11        initiators: List[String], dir: Path, deps: Deps, strs: List[String]): Deps =
    14.1 --- a/src/Pure/Thy/thy_load.scala	Fri Aug 12 09:17:30 2011 -0700
    14.2 +++ b/src/Pure/Thy/thy_load.scala	Fri Aug 12 23:29:28 2011 +0200
    14.3 @@ -10,6 +10,6 @@
    14.4  {
    14.5    def is_loaded(name: String): Boolean
    14.6  
    14.7 -  def check_thy(dir: Path, name: String): (String, Thy_Header.Header)
    14.8 +  def check_thy(dir: Path, name: String): (String, Thy_Header)
    14.9  }
   14.10  
    15.1 --- a/src/Pure/Thy/thy_syntax.scala	Fri Aug 12 09:17:30 2011 -0700
    15.2 +++ b/src/Pure/Thy/thy_syntax.scala	Fri Aug 12 23:29:28 2011 +0200
    15.3 @@ -203,9 +203,9 @@
    15.4            val node = nodes(name)
    15.5            val update_header =
    15.6              (node.header.thy_header, header) match {
    15.7 -              case (Exn.Res(thy_header0), Document.Node.Header(_, Exn.Res(thy_header)))
    15.8 -              if thy_header0 != thy_header => true
    15.9 -              case (Exn.Exn(_), Document.Node.Header(_, Exn.Res(thy_header))) => true
   15.10 +              case (Exn.Res(thy_header0), Document.Node.Header(_, Exn.Res(thy_header))) =>
   15.11 +                thy_header0 != thy_header
   15.12 +              case _ => true
   15.13              }
   15.14            if (update_header) doc_edits += (name -> Document.Node.Update_Header(header))
   15.15        }
    16.1 --- a/src/Pure/library.scala	Fri Aug 12 09:17:30 2011 -0700
    16.2 +++ b/src/Pure/library.scala	Fri Aug 12 23:29:28 2011 +0200
    16.3 @@ -20,19 +20,12 @@
    16.4  {
    16.5    /* user errors */
    16.6  
    16.7 -  private val runtime_exception = Class.forName("java.lang.RuntimeException")
    16.8 -
    16.9    object ERROR
   16.10    {
   16.11      def apply(message: String): Throwable = new RuntimeException(message)
   16.12      def unapply(exn: Throwable): Option[String] =
   16.13        exn match {
   16.14 -        case e: RuntimeException =>
   16.15 -          if (e.getClass != runtime_exception) Some(e.toString)
   16.16 -          else {
   16.17 -            val msg = e.getMessage
   16.18 -            Some(if (msg == null) "Error" else msg)
   16.19 -          }
   16.20 +        case e: RuntimeException => Some(Exn.message(e))
   16.21          case _ => None
   16.22        }
   16.23    }
    17.1 --- a/src/Tools/jEdit/src/document_model.scala	Fri Aug 12 09:17:30 2011 -0700
    17.2 +++ b/src/Tools/jEdit/src/document_model.scala	Fri Aug 12 23:29:28 2011 +0200
    17.3 @@ -45,10 +45,11 @@
    17.4      }
    17.5    }
    17.6  
    17.7 -  def init(session: Session, buffer: Buffer, master_dir: Path, thy_name: String): Document_Model =
    17.8 +  def init(session: Session, buffer: Buffer,
    17.9 +    master_dir: String, node_name: String, thy_name: String): Document_Model =
   17.10    {
   17.11      exit(buffer)
   17.12 -    val model = new Document_Model(session, buffer, master_dir, thy_name)
   17.13 +    val model = new Document_Model(session, buffer, master_dir, node_name, thy_name)
   17.14      buffer.setProperty(key, model)
   17.15      model.activate()
   17.16      model
   17.17 @@ -56,15 +57,13 @@
   17.18  }
   17.19  
   17.20  
   17.21 -class Document_Model(val session: Session,
   17.22 -  val buffer: Buffer, val master_dir: Path, val thy_name: String)
   17.23 +class Document_Model(val session: Session, val buffer: Buffer,
   17.24 +  val master_dir: String, val node_name: String, val thy_name: String)
   17.25  {
   17.26    /* pending text edits */
   17.27  
   17.28 -  private val node_name = (master_dir + Path.basic(thy_name)).implode
   17.29 -
   17.30 -  private def node_header(): Document.Node.Header =
   17.31 -    Document.Node.Header(Path.current,  // FIXME master_dir (!?)
   17.32 +  def node_header(): Document.Node.Header =
   17.33 +    Document.Node.Header(master_dir,
   17.34        Exn.capture { Thy_Header.check(thy_name, buffer.getSegment(0, buffer.getLength)) })
   17.35  
   17.36    private object pending_edits  // owned by Swing thread
    18.1 --- a/src/Tools/jEdit/src/plugin.scala	Fri Aug 12 09:17:30 2011 -0700
    18.2 +++ b/src/Tools/jEdit/src/plugin.scala	Fri Aug 12 23:29:28 2011 +0200
    18.3 @@ -23,6 +23,7 @@
    18.4  import org.gjt.sp.jedit.syntax.{Token => JEditToken, ModeProvider}
    18.5  import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged}
    18.6  import org.gjt.sp.jedit.gui.DockableWindowManager
    18.7 +import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSManager}
    18.8  
    18.9  import org.gjt.sp.util.SyntaxUtilities
   18.10  import org.gjt.sp.util.Log
   18.11 @@ -185,6 +186,15 @@
   18.12    def buffer_text(buffer: JEditBuffer): String =
   18.13      buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
   18.14  
   18.15 +  def buffer_path(buffer: Buffer): (String, String) =
   18.16 +  {
   18.17 +    val master_dir = buffer.getDirectory
   18.18 +    val path = buffer.getSymlinkPath
   18.19 +    if (VFSManager.getVFSForPath(path).isInstanceOf[FileVFS])
   18.20 +      (Isabelle_System.posix_path(master_dir), Isabelle_System.posix_path(path))
   18.21 +    else (master_dir, path)
   18.22 +  }
   18.23 +
   18.24  
   18.25    /* document model and view */
   18.26  
   18.27 @@ -198,16 +208,11 @@
   18.28          document_model(buffer) match {
   18.29            case Some(model) => Some(model)
   18.30            case None =>
   18.31 -            // FIXME strip protocol prefix of URL
   18.32 -            {
   18.33 -              try {
   18.34 -                Some(Thy_Header.split_thy_path(
   18.35 -                  Path.explode(Isabelle_System.posix_path(buffer.getPath))))
   18.36 -              }
   18.37 -              catch { case _ => None }
   18.38 -            } map {
   18.39 -              case (master_dir, thy_name) =>
   18.40 -                Document_Model.init(session, buffer, master_dir, thy_name)
   18.41 +            val (master_dir, path) = buffer_path(buffer)
   18.42 +            Thy_Header.thy_name(path) match {
   18.43 +              case Some(name) =>
   18.44 +                Some(Document_Model.init(session, buffer, master_dir, path, name))
   18.45 +              case None => None
   18.46              }
   18.47          }
   18.48        if (opt_model.isDefined) {
   18.49 @@ -322,15 +327,20 @@
   18.50  
   18.51    private val file_store = new Session.File_Store
   18.52    {
   18.53 -    def read(path: Path): String =
   18.54 +    def append(master_dir: String, path: Path): String =
   18.55      {
   18.56 -      val platform_path = Isabelle_System.platform_path(path)
   18.57 -      val canonical_path = MiscUtilities.resolveSymlinks(platform_path)
   18.58 +      val vfs = VFSManager.getVFSForPath(master_dir)
   18.59 +      if (vfs.isInstanceOf[FileVFS])
   18.60 +        MiscUtilities.resolveSymlinks(
   18.61 +          vfs.constructPath(master_dir, Isabelle_System.platform_path(path)))
   18.62 +      else vfs.constructPath(master_dir, Isabelle_System.standard_path(path))
   18.63 +    }
   18.64  
   18.65 -      Isabelle.jedit_buffers().find(buffer =>
   18.66 -          MiscUtilities.resolveSymlinks(buffer.getPath) == canonical_path) match {
   18.67 -        case Some(buffer) => Isabelle.buffer_text(buffer)
   18.68 -        case None => Standard_System.read_file(new File(platform_path))
   18.69 +    def require(canonical_name: String)
   18.70 +    {
   18.71 +      Swing_Thread.later {
   18.72 +        if (!Isabelle.jedit_buffers().exists(_.getSymlinkPath == canonical_name))
   18.73 +          jEdit.openFile(null: View, canonical_name)
   18.74        }
   18.75      }
   18.76    }