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 }