explicit master_dir as part of header -- still required (for Cygwin) since Scala layer does not pass file content yet;
--- a/src/Pure/PIDE/document.ML Sun Sep 18 16:33:30 2011 +0200
+++ b/src/Pure/PIDE/document.ML Sun Sep 18 19:49:35 2011 +0200
@@ -15,7 +15,7 @@
val new_id: unit -> id
val parse_id: string -> id
val print_id: id -> string
- type node_header = (string * string list * (string * bool) list) Exn.result
+ type node_header = ((string * string) * string list * (string * bool) list) Exn.result
datatype node_edit =
Clear |
Edits of (command_id option * command_id option) list |
@@ -58,7 +58,7 @@
(** document structure **)
-type node_header = (string * string list * (string * bool) list) Exn.result;
+type node_header = ((string * string) * string list * (string * bool) list) Exn.result;
type perspective = (command_id -> bool) * command_id option; (*visible commands, last*)
structure Entries = Linear_Set(type key = command_id val ord = int_ord);
@@ -435,14 +435,11 @@
is_some (Thy_Info.lookup_theory name) orelse (* FIXME more robust!? *)
is_some (Exn.get_res (get_header (get_node nodes name)));
-fun init_theory deps name node =
+fun init_theory deps node =
let
- val (thy_name, imports, uses) = Exn.release (get_header node);
- (* FIXME provide files via Scala layer *)
- val (dir, files) =
- if ML_System.platform_is_cygwin then (Path.current, [])
- else (Path.dir (Path.explode name), map (apfst Path.explode) uses);
-
+ (* FIXME provide files via Scala layer, not master_dir *)
+ val ((master_dir, thy_name), imports, uses) = Exn.release (get_header node);
+ val files = map (apfst Path.explode) uses;
val parents =
imports |> map (fn import =>
(case Thy_Info.lookup_theory import of (* FIXME more robust!? *)
@@ -450,7 +447,7 @@
| NONE =>
get_theory (Position.file_only import)
(snd (Future.join (the (AList.lookup (op =) deps import))))));
- in Thy_Load.begin_theory dir thy_name imports files parents end;
+ in Thy_Load.begin_theory (Path.explode master_dir) thy_name imports files parents end;
in
@@ -471,7 +468,7 @@
else
let
val node0 = node_of old_version name;
- fun init () = init_theory deps name node;
+ fun init () = init_theory deps node;
val bad_init =
not (check_theory nodes name andalso forall (check_theory nodes o #1) deps);
in
--- a/src/Pure/PIDE/isar_document.ML Sun Sep 18 16:33:30 2011 +0200
+++ b/src/Pure/PIDE/isar_document.ML Sun Sep 18 19:49:35 2011 +0200
@@ -47,7 +47,8 @@
fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
fn ([], a) =>
Document.Header
- (Exn.Res (triple string (list string) (list (pair string bool)) a)),
+ (Exn.Res
+ (triple (pair string string) (list string) (list (pair string bool)) a)),
fn ([a], []) => Document.Header (Exn.Exn (ERROR a)),
fn (a, []) => Document.Perspective (map int_atom a)]))
end;
--- a/src/Pure/PIDE/isar_document.scala Sun Sep 18 16:33:30 2011 +0200
+++ b/src/Pure/PIDE/isar_document.scala Sun Sep 18 19:49:35 2011 +0200
@@ -191,17 +191,24 @@
val edits_yxml =
{ import XML.Encode._
def id: T[Command] = (cmd => long(cmd.id))
- def encode: T[List[Document.Edit_Command]] =
- list(pair((name => string(name.node)),
- variant(List(
- { case Document.Node.Clear() => (Nil, Nil) },
- { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
- { case Document.Node.Header(Exn.Res(Thy_Header(a, b, c))) =>
- (Nil, triple(string, list(string), list(pair(string, bool)))(a, b, c)) },
- { case Document.Node.Header(Exn.Exn(e)) => (List(Exn.message(e)), Nil) },
- { case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) }))))
+ def encode_edit(dir: String)
+ : T[Document.Node.Edit[(Option[Command], Option[Command]), Command.Perspective]] =
+ variant(List(
+ { case Document.Node.Clear() => (Nil, Nil) },
+ { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
+ { case Document.Node.Header(Exn.Res(Thy_Header(a, b, c))) =>
+ (Nil,
+ triple(pair(string, string), list(string), list(pair(string, bool)))(
+ (dir, a), b, c)) },
+ { case Document.Node.Header(Exn.Exn(e)) => (List(Exn.message(e)), Nil) },
+ { case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) }))
+ def encode: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) =>
+ {
+ val (name, edit) = node_edit
+ val dir = Isabelle_System.posix_path(name.dir)
+ pair(string, encode_edit(dir))(name.node, edit)
+ })
YXML.string_of_body(encode(edits)) }
-
input("Isar_Document.update", Document.ID(old_id), Document.ID(new_id), edits_yxml)
}