merged
authorhuffman
Fri Aug 12 16:47:53 2011 -0700 (2011-08-12)
changeset 4417528cdf93076f4
parent 44174 d1d79f0e1ea6
parent 44173 aaaa13e297dc
child 44176 eda112e9cdee
merged
     1.1 --- a/src/Pure/Concurrent/future.ML	Fri Aug 12 14:45:50 2011 -0700
     1.2 +++ b/src/Pure/Concurrent/future.ML	Fri Aug 12 16:47:53 2011 -0700
     1.3 @@ -310,7 +310,7 @@
     1.4      val _ =
     1.5        if mm = 0 orelse ! worker_trend > 50 orelse ! worker_trend < ~50 then
     1.6          max_workers := mm
     1.7 -      else if ! worker_trend > 5 andalso ! max_workers < 2 * m then
     1.8 +      else if ! worker_trend > 5 andalso ! max_workers < 2 * m orelse ! max_workers = 0 then
     1.9          max_workers := Int.min (mm, 2 * m)
    1.10        else ();
    1.11  
    1.12 @@ -358,11 +358,11 @@
    1.13      else reraise exn;
    1.14  
    1.15  fun scheduler_loop () =
    1.16 -  while
    1.17 + (while
    1.18      Multithreading.with_attributes
    1.19        (Multithreading.sync_interrupts Multithreading.public_interrupts)
    1.20        (fn _ => SYNCHRONIZED "scheduler" (fn () => scheduler_next ()))
    1.21 -  do ();
    1.22 +  do (); last_round := Time.zeroTime);
    1.23  
    1.24  fun scheduler_active () = (*requires SYNCHRONIZED*)
    1.25    (case ! scheduler of NONE => false | SOME thread => Thread.isActive thread);
     2.1 --- a/src/Pure/General/exn.ML	Fri Aug 12 14:45:50 2011 -0700
     2.2 +++ b/src/Pure/General/exn.ML	Fri Aug 12 16:47:53 2011 -0700
     2.3 @@ -30,7 +30,7 @@
     2.4  structure Exn: EXN =
     2.5  struct
     2.6  
     2.7 -(* runtime exceptions as values *)
     2.8 +(* exceptions as values *)
     2.9  
    2.10  datatype 'a result =
    2.11    Res of 'a |
     3.1 --- a/src/Pure/General/exn.scala	Fri Aug 12 14:45:50 2011 -0700
     3.2 +++ b/src/Pure/General/exn.scala	Fri Aug 12 16:47:53 2011 -0700
     3.3 @@ -9,7 +9,7 @@
     3.4  
     3.5  object Exn
     3.6  {
     3.7 -  /* runtime exceptions as values */
     3.8 +  /* exceptions as values */
     3.9  
    3.10    sealed abstract class Result[A]
    3.11    case class Res[A](res: A) extends Result[A]
    3.12 @@ -24,5 +24,17 @@
    3.13        case Res(x) => x
    3.14        case Exn(exn) => throw exn
    3.15      }
    3.16 +
    3.17 +
    3.18 +  /* message */
    3.19 +
    3.20 +  private val runtime_exception = Class.forName("java.lang.RuntimeException")
    3.21 +
    3.22 +  def message(exn: Throwable): String =
    3.23 +    if (exn.getClass == runtime_exception) {
    3.24 +      val msg = exn.getMessage
    3.25 +      if (msg == null) "Error" else msg
    3.26 +    }
    3.27 +    else exn.toString
    3.28  }
    3.29  
     4.1 --- a/src/Pure/General/graph.ML	Fri Aug 12 14:45:50 2011 -0700
     4.2 +++ b/src/Pure/General/graph.ML	Fri Aug 12 16:47:53 2011 -0700
     4.3 @@ -49,6 +49,8 @@
     4.4    val topological_order: 'a T -> key list
     4.5    val add_edge_trans_acyclic: key * key -> 'a T -> 'a T               (*exception CYCLES*)
     4.6    val merge_trans_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T   (*exception CYCLES*)
     4.7 +  exception DEP of key * key
     4.8 +  val schedule: ((key * 'b) list -> key * 'a -> 'b) -> 'a T -> 'b list  (*exception DEP*)
     4.9  end;
    4.10  
    4.11  functor Graph(Key: KEY): GRAPH =
    4.12 @@ -285,6 +287,24 @@
    4.13      |> fold add_edge_trans_acyclic (diff_edges G2 G1);
    4.14  
    4.15  
    4.16 +(* schedule acyclic graph *)
    4.17 +
    4.18 +exception DEP of key * key;
    4.19 +
    4.20 +fun schedule f G =
    4.21 +  let
    4.22 +    val xs = topological_order G;
    4.23 +    val results = (xs, Table.empty) |-> fold (fn x => fn tab =>
    4.24 +      let
    4.25 +        val a = get_node G x;
    4.26 +        val deps = imm_preds G x |> map (fn y =>
    4.27 +          (case Table.lookup tab y of
    4.28 +            SOME b => (y, b)
    4.29 +          | NONE => raise DEP (x, y)));
    4.30 +      in Table.update (x, f deps (x, a)) tab end);
    4.31 +  in map (the o Table.lookup results) xs end;
    4.32 +
    4.33 +
    4.34  (*final declarations of this structure!*)
    4.35  val map = map_nodes;
    4.36  val fold = fold_graph;
     5.1 --- a/src/Pure/General/path.ML	Fri Aug 12 14:45:50 2011 -0700
     5.2 +++ b/src/Pure/General/path.ML	Fri Aug 12 16:47:53 2011 -0700
     5.3 @@ -51,7 +51,7 @@
     5.4    | check_elem (chs as ["~"]) = err_elem "Illegal" chs
     5.5    | check_elem (chs as ["~", "~"]) = err_elem "Illegal" chs
     5.6    | check_elem chs =
     5.7 -      (case inter (op =) ["/", "\\", "$", ":"] chs of
     5.8 +      (case inter (op =) ["/", "\\", ":"] chs of
     5.9          [] => chs
    5.10        | bads => err_elem ("Illegal character(s) " ^ commas_quote bads ^ " in") chs);
    5.11  
     6.1 --- a/src/Pure/PIDE/document.ML	Fri Aug 12 14:45:50 2011 -0700
     6.2 +++ b/src/Pure/PIDE/document.ML	Fri Aug 12 16:47:53 2011 -0700
     6.3 @@ -249,14 +249,13 @@
     6.4  
     6.5  in
     6.6  
     6.7 -fun run_command thy_name raw_tr st =
     6.8 +fun run_command node_name raw_tr st =
     6.9    (case
    6.10        (case Toplevel.init_of raw_tr of
    6.11 -        SOME name => Exn.capture (fn () =>
    6.12 -          let
    6.13 -            val path = Path.explode thy_name;
    6.14 -            val _ = Thy_Header.consistent_name (Path.implode (Path.base path)) name;
    6.15 -          in Toplevel.modify_master (SOME (Path.dir path)) raw_tr end) ()
    6.16 +        SOME name =>
    6.17 +          Exn.capture (fn () =>
    6.18 +            let val master_dir = Path.dir (Path.explode node_name);  (* FIXME move to Scala side *)
    6.19 +            in Toplevel.modify_master (SOME master_dir) raw_tr end) ()
    6.20        | NONE => Exn.Res raw_tr) of
    6.21      Exn.Res tr =>
    6.22        let
     7.1 --- a/src/Pure/PIDE/document.scala	Fri Aug 12 14:45:50 2011 -0700
     7.2 +++ b/src/Pure/PIDE/document.scala	Fri Aug 12 16:47:53 2011 -0700
     7.3 @@ -51,8 +51,17 @@
     7.4      case class Edits[A](edits: List[A]) extends Edit[A]
     7.5      case class Update_Header[A](header: Header) extends Edit[A]
     7.6  
     7.7 -    sealed case class Header(val master_dir: Path, val thy_header: Exn.Result[Thy_Header.Header])
     7.8 -    val empty_header = Header(Path.current, Exn.Exn(ERROR("Bad theory header")))
     7.9 +    sealed case class Header(val master_dir: String, val thy_header: Exn.Result[Thy_Header])
    7.10 +    {
    7.11 +      def norm_deps(f: (String, Path) => String): Header =
    7.12 +        copy(thy_header =
    7.13 +          thy_header match {
    7.14 +            case Exn.Res(header) =>
    7.15 +              Exn.capture { header.norm_deps(name => f(master_dir, Path.explode(name))) }
    7.16 +            case exn => exn
    7.17 +          })
    7.18 +    }
    7.19 +    val empty_header = Header("", Exn.Exn(ERROR("Bad theory header")))
    7.20  
    7.21      val empty: Node = Node(empty_header, Map(), Linear_Set())
    7.22  
     8.1 --- a/src/Pure/PIDE/isar_document.scala	Fri Aug 12 14:45:50 2011 -0700
     8.2 +++ b/src/Pure/PIDE/isar_document.scala	Fri Aug 12 16:47:53 2011 -0700
     8.3 @@ -150,10 +150,10 @@
     8.4              { case Document.Node.Remove() => (Nil, Nil) },
     8.5              { case Document.Node.Edits(a) => (Nil, list(pair(option(long), option(long)))(a)) },
     8.6              { case Document.Node.Update_Header(
     8.7 -                  Document.Node.Header(_, Exn.Res(Thy_Header.Header(a, b, c)))) =>
     8.8 +                  Document.Node.Header(_, Exn.Res(Thy_Header(a, b, c)))) =>
     8.9                  (Nil, triple(string, list(string), list(string))(a, b, c)) },
    8.10              { case Document.Node.Update_Header(
    8.11 -                  Document.Node.Header(_, Exn.Exn(ERROR(a)))) => (List(a), Nil) }))))
    8.12 +                  Document.Node.Header(_, Exn.Exn(e))) => (List(Exn.message(e)), Nil) }))))
    8.13        YXML.string_of_body(encode(edits)) }
    8.14  
    8.15      input("Isar_Document.edit_version", Document.ID(old_id), Document.ID(new_id), edits_yxml)
     9.1 --- a/src/Pure/System/invoke_scala.scala	Fri Aug 12 14:45:50 2011 -0700
     9.2 +++ b/src/Pure/System/invoke_scala.scala	Fri Aug 12 16:47:53 2011 -0700
     9.3 @@ -57,10 +57,8 @@
     9.4          Exn.capture { f(arg) } match {
     9.5            case Exn.Res(null) => (Tag.NULL, "")
     9.6            case Exn.Res(res) => (Tag.OK, res)
     9.7 -          case Exn.Exn(ERROR(msg)) => (Tag.ERROR, msg)
     9.8 -          case Exn.Exn(e) => (Tag.ERROR, e.toString)
     9.9 +          case Exn.Exn(e) => (Tag.ERROR, Exn.message(e))
    9.10          }
    9.11 -      case Exn.Exn(ERROR(msg)) => (Tag.FAIL, msg)
    9.12 -      case Exn.Exn(e) => (Tag.FAIL, e.toString)
    9.13 +      case Exn.Exn(e) => (Tag.FAIL, Exn.message(e))
    9.14      }
    9.15  }
    10.1 --- a/src/Pure/System/session.scala	Fri Aug 12 14:45:50 2011 -0700
    10.2 +++ b/src/Pure/System/session.scala	Fri Aug 12 16:47:53 2011 -0700
    10.3 @@ -20,7 +20,8 @@
    10.4  
    10.5    abstract class File_Store
    10.6    {
    10.7 -    def read(path: Path): String
    10.8 +    def append(master_dir: String, path: Path): String
    10.9 +    def require(file: String): Unit
   10.10    }
   10.11  
   10.12  
   10.13 @@ -146,7 +147,7 @@
   10.14      override def is_loaded(name: String): Boolean =
   10.15        loaded_theories.contains(name)
   10.16  
   10.17 -    override def check_thy(dir: Path, name: String): (String, Thy_Header.Header) =
   10.18 +    override def check_thy(dir: Path, name: String): (String, Thy_Header) =
   10.19      {
   10.20        val file = Isabelle_System.platform_file(dir + Thy_Header.thy_path(name))
   10.21        if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
   10.22 @@ -186,7 +187,8 @@
   10.23        val syntax = current_syntax()
   10.24        val previous = global_state().history.tip.version
   10.25        val doc_edits =
   10.26 -        (name, Document.Node.Update_Header[Text.Edit](header)) :: edits.map(edit => (name, edit))
   10.27 +        (name, Document.Node.Update_Header[Text.Edit](header.norm_deps(file_store.append))) ::
   10.28 +          edits.map(edit => (name, edit))
   10.29        val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, doc_edits) }
   10.30        val change =
   10.31          global_state.change_yield(_.extend_history(previous, doc_edits, result.map(_._2)))
    11.1 --- a/src/Pure/Thy/thy_header.ML	Fri Aug 12 14:45:50 2011 -0700
    11.2 +++ b/src/Pure/Thy/thy_header.ML	Fri Aug 12 16:47:53 2011 -0700
    11.3 @@ -9,7 +9,6 @@
    11.4    val args: Token.T list -> (string * string list * (string * bool) list) * Token.T list
    11.5    val read: Position.T -> string -> string * string list * (Path.T * bool) list
    11.6    val thy_path: string -> Path.T
    11.7 -  val split_thy_path: Path.T -> Path.T * string
    11.8    val consistent_name: string -> string -> unit
    11.9  end;
   11.10  
   11.11 @@ -73,11 +72,6 @@
   11.12  
   11.13  val thy_path = Path.ext "thy" o Path.basic;
   11.14  
   11.15 -fun split_thy_path path =
   11.16 -  (case Path.split_ext path of
   11.17 -    (path', "thy") => (Path.dir path', Path.implode (Path.base path'))
   11.18 -  | _ => error ("Bad theory file specification: " ^ Path.print path));
   11.19 -
   11.20  fun consistent_name name name' =
   11.21    if name = name' then ()
   11.22    else error ("Bad file name " ^ Path.print (thy_path name) ^ " for theory " ^ quote name');
    12.1 --- a/src/Pure/Thy/thy_header.scala	Fri Aug 12 14:45:50 2011 -0700
    12.2 +++ b/src/Pure/Thy/thy_header.scala	Fri Aug 12 16:47:53 2011 -0700
    12.3 @@ -25,27 +25,20 @@
    12.4  
    12.5    val lexicon = Scan.Lexicon("%", "(", ")", ";", BEGIN, HEADER, IMPORTS, THEORY, USES)
    12.6  
    12.7 -  sealed case class Header(val name: String, val imports: List[String], val uses: List[String])
    12.8 -  {
    12.9 -    def map(f: String => String): Header =
   12.10 -      Header(f(name), imports.map(f), uses.map(f))
   12.11 -  }
   12.12 +
   12.13 +  /* theory file name */
   12.14  
   12.15 +  private val Thy_Name = new Regex(""".*?([^/\\:]+)\.thy""")
   12.16  
   12.17 -  /* file name */
   12.18 +  def thy_name(s: String): Option[String] =
   12.19 +    s match { case Thy_Name(name) => Some(name) case _ => None }
   12.20  
   12.21    def thy_path(name: String): Path = Path.basic(name).ext("thy")
   12.22  
   12.23 -  def split_thy_path(path: Path): (Path, String) =
   12.24 -    path.split_ext match {
   12.25 -      case (path1, "thy") => (path1.dir, path1.base.implode)
   12.26 -      case _ => error("Bad theory file specification: " + path)
   12.27 -    }
   12.28 -
   12.29  
   12.30    /* header */
   12.31  
   12.32 -  val header: Parser[Header] =
   12.33 +  val header: Parser[Thy_Header] =
   12.34    {
   12.35      val file_name = atom("file name", _.is_name)
   12.36      val theory_name = atom("theory name", _.is_name)
   12.37 @@ -57,7 +50,7 @@
   12.38  
   12.39      val args =
   12.40        theory_name ~ (keyword(IMPORTS) ~! (rep1(theory_name) ~ uses ~ keyword(BEGIN))) ^^
   12.41 -        { case x ~ (_ ~ (ys ~ zs ~ _)) => Header(x, ys, zs) }
   12.42 +        { case x ~ (_ ~ (ys ~ zs ~ _)) => Thy_Header(x, ys, zs) }
   12.43  
   12.44      (keyword(HEADER) ~ tags) ~!
   12.45        ((doc_source ~ rep(keyword(";")) ~ keyword(THEORY) ~ tags) ~> args) ^^ { case _ ~ x => x } |
   12.46 @@ -67,7 +60,7 @@
   12.47  
   12.48    /* read -- lazy scanning */
   12.49  
   12.50 -  def read(reader: Reader[Char]): Header =
   12.51 +  def read(reader: Reader[Char]): Thy_Header =
   12.52    {
   12.53      val token = lexicon.token(_ => false)
   12.54      val toks = new mutable.ListBuffer[Token]
   12.55 @@ -89,10 +82,10 @@
   12.56      }
   12.57    }
   12.58  
   12.59 -  def read(source: CharSequence): Header =
   12.60 +  def read(source: CharSequence): Thy_Header =
   12.61      read(new CharSequenceReader(source))
   12.62  
   12.63 -  def read(file: File): Header =
   12.64 +  def read(file: File): Thy_Header =
   12.65    {
   12.66      val reader = Scan.byte_reader(file)
   12.67      try { read(reader).map(Standard_System.decode_permissive_utf8) }
   12.68 @@ -102,7 +95,7 @@
   12.69  
   12.70    /* check */
   12.71  
   12.72 -  def check(name: String, source: CharSequence): Header =
   12.73 +  def check(name: String, source: CharSequence): Thy_Header =
   12.74    {
   12.75      val header = read(source)
   12.76      val name1 = header.name
   12.77 @@ -111,3 +104,14 @@
   12.78      header
   12.79    }
   12.80  }
   12.81 +
   12.82 +
   12.83 +sealed case class Thy_Header(val name: String, val imports: List[String], val uses: List[String])
   12.84 +{
   12.85 +  def map(f: String => String): Thy_Header =
   12.86 +    Thy_Header(f(name), imports.map(f), uses.map(f))
   12.87 +
   12.88 +  def norm_deps(f: String => String): Thy_Header =
   12.89 +    copy(imports = imports.map(name => f(name) + ".thy"), uses = uses.map(f))
   12.90 +}
   12.91 +
    13.1 --- a/src/Pure/Thy/thy_info.ML	Fri Aug 12 14:45:50 2011 -0700
    13.2 +++ b/src/Pure/Thy/thy_info.ML	Fri Aug 12 16:47:53 2011 -0700
    13.3 @@ -178,51 +178,37 @@
    13.4  fun task_finished (Task _) = false
    13.5    | task_finished (Finished _) = true;
    13.6  
    13.7 +fun task_parents deps (parents: string list) = map (the o AList.lookup (op =) deps) parents;
    13.8 +
    13.9  local
   13.10  
   13.11  fun finish_thy ((thy, present, commit): result) =
   13.12    (Global_Theory.join_proofs thy; Future.join present; commit (); thy);
   13.13  
   13.14 -fun schedule_seq task_graph =
   13.15 -  ((Graph.topological_order task_graph, Symtab.empty) |-> fold (fn name => fn tab =>
   13.16 -    (case Graph.get_node task_graph name of
   13.17 -      Task (parents, body) =>
   13.18 -        let val result = body (map (the o Symtab.lookup tab) parents)
   13.19 -        in Symtab.update (name, finish_thy result) tab end
   13.20 -    | Finished thy => Symtab.update (name, thy) tab))) |> ignore;
   13.21 -
   13.22 -fun schedule_futures task_graph = uninterruptible (fn _ => fn () =>
   13.23 -  let
   13.24 -    val tasks = Graph.topological_order task_graph;
   13.25 -    val futures = (tasks, Symtab.empty) |-> fold (fn name => fn tab =>
   13.26 -      (case Graph.get_node task_graph name of
   13.27 -        Task (parents, body) =>
   13.28 -          let
   13.29 -            val get = the o Symtab.lookup tab;
   13.30 -            val deps = map (`get) (Graph.imm_preds task_graph name);
   13.31 -            val task_deps = map (Future.task_of o #1) deps;
   13.32 -            fun failed (future, parent) = if can Future.join future then NONE else SOME parent;
   13.33 +val schedule_seq =
   13.34 +  Graph.schedule (fn deps => fn (_, task) =>
   13.35 +    (case task of
   13.36 +      Task (parents, body) => finish_thy (body (task_parents deps parents))
   13.37 +    | Finished thy => thy)) #> ignore;
   13.38  
   13.39 -            val future =
   13.40 -              singleton
   13.41 -                (Future.forks
   13.42 -                  {name = "theory:" ^ name, group = NONE, deps = task_deps, pri = 0,
   13.43 -                    interrupts = true})
   13.44 -                (fn () =>
   13.45 -                  (case map_filter failed deps of
   13.46 -                    [] => body (map (#1 o Future.join o get) parents)
   13.47 -                  | bad => error (loader_msg ("failed to load " ^ quote name ^
   13.48 -                      " (unresolved " ^ commas_quote bad ^ ")") [])));
   13.49 -          in Symtab.update (name, future) tab end
   13.50 -      | Finished thy => Symtab.update (name, Future.value (thy, Future.value (), I)) tab));
   13.51 -    val _ =
   13.52 -      tasks |> maps (fn name =>
   13.53 -        let
   13.54 -          val result = Future.join (the (Symtab.lookup futures name));
   13.55 -          val _ = finish_thy result;
   13.56 -        in [] end handle exn => [Exn.Exn exn])
   13.57 -      |> rev |> Exn.release_all;
   13.58 -  in () end) ();
   13.59 +val schedule_futures = uninterruptible (fn _ =>
   13.60 +  Graph.schedule (fn deps => fn (name, task) =>
   13.61 +    (case task of
   13.62 +      Task (parents, body) =>
   13.63 +        singleton
   13.64 +          (Future.forks
   13.65 +            {name = "theory:" ^ name, group = NONE,
   13.66 +              deps = map (Future.task_of o #2) deps,
   13.67 +              pri = 0, interrupts = true})
   13.68 +          (fn () =>
   13.69 +            (case filter (not o can Future.join o #2) deps of
   13.70 +              [] => body (map (#1 o Future.join) (task_parents deps parents))
   13.71 +            | bad =>
   13.72 +                error (loader_msg ("failed to load " ^ quote name ^
   13.73 +                  " (unresolved " ^ commas_quote (map #1 bad) ^ ")") [])))
   13.74 +    | Finished thy => Future.value (thy, Future.value (), I)))
   13.75 +  #> maps (fn result => (finish_thy (Future.join result); []) handle exn => [Exn.Exn exn])
   13.76 +  #> rev #> Exn.release_all) #> ignore;
   13.77  
   13.78  in
   13.79  
    14.1 --- a/src/Pure/Thy/thy_info.scala	Fri Aug 12 14:45:50 2011 -0700
    14.2 +++ b/src/Pure/Thy/thy_info.scala	Fri Aug 12 16:47:53 2011 -0700
    14.3 @@ -38,7 +38,7 @@
    14.4  
    14.5    /* dependencies */
    14.6  
    14.7 -  type Deps = Map[String, Exn.Result[(String, Thy_Header.Header)]]  // name -> (text, header)
    14.8 +  type Deps = Map[String, Exn.Result[(String, Thy_Header)]]  // name -> (text, header)
    14.9  
   14.10    private def require_thys(ignored: String => Boolean,
   14.11        initiators: List[String], dir: Path, deps: Deps, strs: List[String]): Deps =
    15.1 --- a/src/Pure/Thy/thy_load.scala	Fri Aug 12 14:45:50 2011 -0700
    15.2 +++ b/src/Pure/Thy/thy_load.scala	Fri Aug 12 16:47:53 2011 -0700
    15.3 @@ -10,6 +10,6 @@
    15.4  {
    15.5    def is_loaded(name: String): Boolean
    15.6  
    15.7 -  def check_thy(dir: Path, name: String): (String, Thy_Header.Header)
    15.8 +  def check_thy(dir: Path, name: String): (String, Thy_Header)
    15.9  }
   15.10  
    16.1 --- a/src/Pure/Thy/thy_syntax.scala	Fri Aug 12 14:45:50 2011 -0700
    16.2 +++ b/src/Pure/Thy/thy_syntax.scala	Fri Aug 12 16:47:53 2011 -0700
    16.3 @@ -203,9 +203,9 @@
    16.4            val node = nodes(name)
    16.5            val update_header =
    16.6              (node.header.thy_header, header) match {
    16.7 -              case (Exn.Res(thy_header0), Document.Node.Header(_, Exn.Res(thy_header)))
    16.8 -              if thy_header0 != thy_header => true
    16.9 -              case (Exn.Exn(_), Document.Node.Header(_, Exn.Res(thy_header))) => true
   16.10 +              case (Exn.Res(thy_header0), Document.Node.Header(_, Exn.Res(thy_header))) =>
   16.11 +                thy_header0 != thy_header
   16.12 +              case _ => true
   16.13              }
   16.14            if (update_header) doc_edits += (name -> Document.Node.Update_Header(header))
   16.15        }
    17.1 --- a/src/Pure/library.scala	Fri Aug 12 14:45:50 2011 -0700
    17.2 +++ b/src/Pure/library.scala	Fri Aug 12 16:47:53 2011 -0700
    17.3 @@ -20,19 +20,12 @@
    17.4  {
    17.5    /* user errors */
    17.6  
    17.7 -  private val runtime_exception = Class.forName("java.lang.RuntimeException")
    17.8 -
    17.9    object ERROR
   17.10    {
   17.11      def apply(message: String): Throwable = new RuntimeException(message)
   17.12      def unapply(exn: Throwable): Option[String] =
   17.13        exn match {
   17.14 -        case e: RuntimeException =>
   17.15 -          if (e.getClass != runtime_exception) Some(e.toString)
   17.16 -          else {
   17.17 -            val msg = e.getMessage
   17.18 -            Some(if (msg == null) "Error" else msg)
   17.19 -          }
   17.20 +        case e: RuntimeException => Some(Exn.message(e))
   17.21          case _ => None
   17.22        }
   17.23    }
    18.1 --- a/src/Tools/jEdit/src/document_model.scala	Fri Aug 12 14:45:50 2011 -0700
    18.2 +++ b/src/Tools/jEdit/src/document_model.scala	Fri Aug 12 16:47:53 2011 -0700
    18.3 @@ -45,10 +45,11 @@
    18.4      }
    18.5    }
    18.6  
    18.7 -  def init(session: Session, buffer: Buffer, master_dir: Path, thy_name: String): Document_Model =
    18.8 +  def init(session: Session, buffer: Buffer,
    18.9 +    master_dir: String, node_name: String, thy_name: String): Document_Model =
   18.10    {
   18.11      exit(buffer)
   18.12 -    val model = new Document_Model(session, buffer, master_dir, thy_name)
   18.13 +    val model = new Document_Model(session, buffer, master_dir, node_name, thy_name)
   18.14      buffer.setProperty(key, model)
   18.15      model.activate()
   18.16      model
   18.17 @@ -56,15 +57,13 @@
   18.18  }
   18.19  
   18.20  
   18.21 -class Document_Model(val session: Session,
   18.22 -  val buffer: Buffer, val master_dir: Path, val thy_name: String)
   18.23 +class Document_Model(val session: Session, val buffer: Buffer,
   18.24 +  val master_dir: String, val node_name: String, val thy_name: String)
   18.25  {
   18.26    /* pending text edits */
   18.27  
   18.28 -  private val node_name = (master_dir + Path.basic(thy_name)).implode
   18.29 -
   18.30 -  private def node_header(): Document.Node.Header =
   18.31 -    Document.Node.Header(Path.current,  // FIXME master_dir (!?)
   18.32 +  def node_header(): Document.Node.Header =
   18.33 +    Document.Node.Header(master_dir,
   18.34        Exn.capture { Thy_Header.check(thy_name, buffer.getSegment(0, buffer.getLength)) })
   18.35  
   18.36    private object pending_edits  // owned by Swing thread
    19.1 --- a/src/Tools/jEdit/src/plugin.scala	Fri Aug 12 14:45:50 2011 -0700
    19.2 +++ b/src/Tools/jEdit/src/plugin.scala	Fri Aug 12 16:47:53 2011 -0700
    19.3 @@ -23,6 +23,7 @@
    19.4  import org.gjt.sp.jedit.syntax.{Token => JEditToken, ModeProvider}
    19.5  import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged}
    19.6  import org.gjt.sp.jedit.gui.DockableWindowManager
    19.7 +import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSManager}
    19.8  
    19.9  import org.gjt.sp.util.SyntaxUtilities
   19.10  import org.gjt.sp.util.Log
   19.11 @@ -185,6 +186,15 @@
   19.12    def buffer_text(buffer: JEditBuffer): String =
   19.13      buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
   19.14  
   19.15 +  def buffer_path(buffer: Buffer): (String, String) =
   19.16 +  {
   19.17 +    val master_dir = buffer.getDirectory
   19.18 +    val path = buffer.getSymlinkPath
   19.19 +    if (VFSManager.getVFSForPath(path).isInstanceOf[FileVFS])
   19.20 +      (Isabelle_System.posix_path(master_dir), Isabelle_System.posix_path(path))
   19.21 +    else (master_dir, path)
   19.22 +  }
   19.23 +
   19.24  
   19.25    /* document model and view */
   19.26  
   19.27 @@ -198,16 +208,11 @@
   19.28          document_model(buffer) match {
   19.29            case Some(model) => Some(model)
   19.30            case None =>
   19.31 -            // FIXME strip protocol prefix of URL
   19.32 -            {
   19.33 -              try {
   19.34 -                Some(Thy_Header.split_thy_path(
   19.35 -                  Path.explode(Isabelle_System.posix_path(buffer.getPath))))
   19.36 -              }
   19.37 -              catch { case _ => None }
   19.38 -            } map {
   19.39 -              case (master_dir, thy_name) =>
   19.40 -                Document_Model.init(session, buffer, master_dir, thy_name)
   19.41 +            val (master_dir, path) = buffer_path(buffer)
   19.42 +            Thy_Header.thy_name(path) match {
   19.43 +              case Some(name) =>
   19.44 +                Some(Document_Model.init(session, buffer, master_dir, path, name))
   19.45 +              case None => None
   19.46              }
   19.47          }
   19.48        if (opt_model.isDefined) {
   19.49 @@ -322,15 +327,20 @@
   19.50  
   19.51    private val file_store = new Session.File_Store
   19.52    {
   19.53 -    def read(path: Path): String =
   19.54 +    def append(master_dir: String, path: Path): String =
   19.55      {
   19.56 -      val platform_path = Isabelle_System.platform_path(path)
   19.57 -      val canonical_path = MiscUtilities.resolveSymlinks(platform_path)
   19.58 +      val vfs = VFSManager.getVFSForPath(master_dir)
   19.59 +      if (vfs.isInstanceOf[FileVFS])
   19.60 +        MiscUtilities.resolveSymlinks(
   19.61 +          vfs.constructPath(master_dir, Isabelle_System.platform_path(path)))
   19.62 +      else vfs.constructPath(master_dir, Isabelle_System.standard_path(path))
   19.63 +    }
   19.64  
   19.65 -      Isabelle.jedit_buffers().find(buffer =>
   19.66 -          MiscUtilities.resolveSymlinks(buffer.getPath) == canonical_path) match {
   19.67 -        case Some(buffer) => Isabelle.buffer_text(buffer)
   19.68 -        case None => Standard_System.read_file(new File(platform_path))
   19.69 +    def require(canonical_name: String)
   19.70 +    {
   19.71 +      Swing_Thread.later {
   19.72 +        if (!Isabelle.jedit_buffers().exists(_.getSymlinkPath == canonical_name))
   19.73 +          jEdit.openFile(null: View, canonical_name)
   19.74        }
   19.75      }
   19.76    }