# HG changeset patch
# User wenzelm
# Date 1330779889 -3600
# Node ID 44c28a33c461f8b1894a06fa0bf07e79f54c99a9
# Parent  0038386efd8152cb3833f1dfa0e367410348d5a6
retain original "uses" (again) -- still required for Thy_Load.use_file etc. in ML (notably for maintaining required/provided);
tuned;

diff -r 0038386efd81 -r 44c28a33c461 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Sat Mar 03 11:31:12 2012 +0100
+++ b/src/Pure/PIDE/protocol.scala	Sat Mar 03 14:04:49 2012 +0100
@@ -211,19 +211,20 @@
     val edits_yxml =
     { import XML.Encode._
       def id: T[Command] = (cmd => long(cmd.id))
-      def encode_string: T[String] = (s => string(Symbol.encode(s)))
+      def symbol_string: T[String] = (s => string(Symbol.encode(s)))
       def encode_edit(name: Document.Node.Name)
           : 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(deps)) =>
-              val dir = Symbol.encode(Isabelle_System.posix_path(name.dir))
+              val dir = Isabelle_System.posix_path(name.dir)
               val imports = deps.imports.map(_.node)
-              val uses = deps.uses.map(p => (Symbol.encode(Isabelle_System.posix_path(p._1)), p._2))
+              // FIXME val uses = deps.uses.map(p => (Isabelle_System.posix_path(p._1), p._2))
+              val uses = deps.uses
               (Nil,
-                triple(pair(string, encode_string), list(encode_string), list(pair(string, bool)))(
-                  (dir, name.theory), imports, uses)) },
+                triple(pair(symbol_string, symbol_string), list(symbol_string),
+                    list(pair(symbol_string, bool)))((dir, name.theory), imports, uses)) },
           { case Document.Node.Header(Exn.Exn(e)) => (List(Symbol.encode(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) =>
diff -r 0038386efd81 -r 44c28a33c461 src/Pure/Thy/thy_load.scala
--- a/src/Pure/Thy/thy_load.scala	Sat Mar 03 11:31:12 2012 +0100
+++ b/src/Pure/Thy/thy_load.scala	Sat Mar 03 14:04:49 2012 +0100
@@ -57,7 +57,8 @@
   {
     val name1 = header.name
     val imports = header.imports.map(import_name(name.dir, _))
-    val uses = header.uses.map(p => (append(name.dir, Path.explode(p._1)), p._2))
+    // FIXME val uses = header.uses.map(p => (append(name.dir, Path.explode(p._1)), p._2))
+    val uses = header.uses
     if (name.theory != name1)
       error("Bad file name " + thy_path(Path.basic(name.theory)) + " for theory " + quote(name1))
     Document.Node.Deps(imports, uses)