explicit master_dir as part of header -- still required (for Cygwin) since Scala layer does not pass file content yet;
authorwenzelm
Sun Sep 18 19:49:35 2011 +0200 (2011-09-18)
changeset 4497968b990e950b1
parent 44978 a04f3eb3943c
child 44980 ad5883642a83
explicit master_dir as part of header -- still required (for Cygwin) since Scala layer does not pass file content yet;
src/Pure/PIDE/document.ML
src/Pure/PIDE/isar_document.ML
src/Pure/PIDE/isar_document.scala
     1.1 --- a/src/Pure/PIDE/document.ML	Sun Sep 18 16:33:30 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Sun Sep 18 19:49:35 2011 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4    val new_id: unit -> id
     1.5    val parse_id: string -> id
     1.6    val print_id: id -> string
     1.7 -  type node_header = (string * string list * (string * bool) list) Exn.result
     1.8 +  type node_header = ((string * string) * string list * (string * bool) list) Exn.result
     1.9    datatype node_edit =
    1.10      Clear |
    1.11      Edits of (command_id option * command_id option) list |
    1.12 @@ -58,7 +58,7 @@
    1.13  
    1.14  (** document structure **)
    1.15  
    1.16 -type node_header = (string * string list * (string * bool) list) Exn.result;
    1.17 +type node_header = ((string * string) * string list * (string * bool) list) Exn.result;
    1.18  type perspective = (command_id -> bool) * command_id option; (*visible commands, last*)
    1.19  structure Entries = Linear_Set(type key = command_id val ord = int_ord);
    1.20  
    1.21 @@ -435,14 +435,11 @@
    1.22    is_some (Thy_Info.lookup_theory name) orelse  (* FIXME more robust!? *)
    1.23    is_some (Exn.get_res (get_header (get_node nodes name)));
    1.24  
    1.25 -fun init_theory deps name node =
    1.26 +fun init_theory deps node =
    1.27    let
    1.28 -    val (thy_name, imports, uses) = Exn.release (get_header node);
    1.29 -    (* FIXME provide files via Scala layer *)
    1.30 -    val (dir, files) =
    1.31 -      if ML_System.platform_is_cygwin then (Path.current, [])
    1.32 -      else (Path.dir (Path.explode name), map (apfst Path.explode) uses);
    1.33 -
    1.34 +    (* FIXME provide files via Scala layer, not master_dir *)
    1.35 +    val ((master_dir, thy_name), imports, uses) = Exn.release (get_header node);
    1.36 +    val files = map (apfst Path.explode) uses;
    1.37      val parents =
    1.38        imports |> map (fn import =>
    1.39          (case Thy_Info.lookup_theory import of  (* FIXME more robust!? *)
    1.40 @@ -450,7 +447,7 @@
    1.41          | NONE =>
    1.42              get_theory (Position.file_only import)
    1.43                (snd (Future.join (the (AList.lookup (op =) deps import))))));
    1.44 -  in Thy_Load.begin_theory dir thy_name imports files parents end;
    1.45 +  in Thy_Load.begin_theory (Path.explode master_dir) thy_name imports files parents end;
    1.46  
    1.47  in
    1.48  
    1.49 @@ -471,7 +468,7 @@
    1.50            else
    1.51              let
    1.52                val node0 = node_of old_version name;
    1.53 -              fun init () = init_theory deps name node;
    1.54 +              fun init () = init_theory deps node;
    1.55                val bad_init =
    1.56                  not (check_theory nodes name andalso forall (check_theory nodes o #1) deps);
    1.57              in
     2.1 --- a/src/Pure/PIDE/isar_document.ML	Sun Sep 18 16:33:30 2011 +0200
     2.2 +++ b/src/Pure/PIDE/isar_document.ML	Sun Sep 18 19:49:35 2011 +0200
     2.3 @@ -47,7 +47,8 @@
     2.4                    fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
     2.5                    fn ([], a) =>
     2.6                      Document.Header
     2.7 -                      (Exn.Res (triple string (list string) (list (pair string bool)) a)),
     2.8 +                      (Exn.Res
     2.9 +                        (triple (pair string string) (list string) (list (pair string bool)) a)),
    2.10                    fn ([a], []) => Document.Header (Exn.Exn (ERROR a)),
    2.11                    fn (a, []) => Document.Perspective (map int_atom a)]))
    2.12              end;
     3.1 --- a/src/Pure/PIDE/isar_document.scala	Sun Sep 18 16:33:30 2011 +0200
     3.2 +++ b/src/Pure/PIDE/isar_document.scala	Sun Sep 18 19:49:35 2011 +0200
     3.3 @@ -191,17 +191,24 @@
     3.4      val edits_yxml =
     3.5      { import XML.Encode._
     3.6        def id: T[Command] = (cmd => long(cmd.id))
     3.7 -      def encode: T[List[Document.Edit_Command]] =
     3.8 -        list(pair((name => string(name.node)),
     3.9 -          variant(List(
    3.10 -            { case Document.Node.Clear() => (Nil, Nil) },
    3.11 -            { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
    3.12 -            { case Document.Node.Header(Exn.Res(Thy_Header(a, b, c))) =>
    3.13 -                (Nil, triple(string, list(string), list(pair(string, bool)))(a, b, c)) },
    3.14 -            { case Document.Node.Header(Exn.Exn(e)) => (List(Exn.message(e)), Nil) },
    3.15 -            { case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) }))))
    3.16 +      def encode_edit(dir: String)
    3.17 +          : T[Document.Node.Edit[(Option[Command], Option[Command]), Command.Perspective]] =
    3.18 +        variant(List(
    3.19 +          { case Document.Node.Clear() => (Nil, Nil) },
    3.20 +          { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
    3.21 +          { case Document.Node.Header(Exn.Res(Thy_Header(a, b, c))) =>
    3.22 +              (Nil,
    3.23 +                triple(pair(string, string), list(string), list(pair(string, bool)))(
    3.24 +                  (dir, a), b, c)) },
    3.25 +          { case Document.Node.Header(Exn.Exn(e)) => (List(Exn.message(e)), Nil) },
    3.26 +          { case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) }))
    3.27 +      def encode: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) =>
    3.28 +      {
    3.29 +        val (name, edit) = node_edit
    3.30 +        val dir = Isabelle_System.posix_path(name.dir)
    3.31 +        pair(string, encode_edit(dir))(name.node, edit)
    3.32 +      })
    3.33        YXML.string_of_body(encode(edits)) }
    3.34 -
    3.35      input("Isar_Document.update", Document.ID(old_id), Document.ID(new_id), edits_yxml)
    3.36    }
    3.37