# HG changeset patch
# User wenzelm
# Date 1087298642 -7200
# Node ID e22fad2b6f6fa44e8e001aefac310cddc4bc7f8d
# Parent  5f5605361aad12030ea9884b6e9c104e2e0807cf
path instead of string;

diff -r 5f5605361aad -r e22fad2b6f6f src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Tue Jun 15 13:23:39 2004 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Jun 15 13:24:02 2004 +0200
@@ -30,18 +30,18 @@
   val undo: Toplevel.transition -> Toplevel.transition
   val kill: Toplevel.transition -> Toplevel.transition
   val back: bool -> Toplevel.transition -> Toplevel.transition
-  val use: string -> Toplevel.transition -> Toplevel.transition
+  val use: Path.T -> Toplevel.transition -> Toplevel.transition
   val use_mltext_theory: string -> Toplevel.transition -> Toplevel.transition
   val use_mltext: bool -> string -> Toplevel.transition -> Toplevel.transition
   val use_commit: Toplevel.transition -> Toplevel.transition
-  val cd: string -> Toplevel.transition -> Toplevel.transition
+  val cd: Path.T -> Toplevel.transition -> Toplevel.transition
   val pwd: Toplevel.transition -> Toplevel.transition
   val use_thy: string -> Toplevel.transition -> Toplevel.transition
   val use_thy_only: string -> Toplevel.transition -> Toplevel.transition
   val update_thy: string -> Toplevel.transition -> Toplevel.transition
   val update_thy_only: string -> Toplevel.transition -> Toplevel.transition
-  val display_drafts: string list -> Toplevel.transition -> Toplevel.transition
-  val print_drafts: string list -> Toplevel.transition -> Toplevel.transition
+  val display_drafts: Path.T list -> Toplevel.transition -> Toplevel.transition
+  val print_drafts: Path.T list -> Toplevel.transition -> Toplevel.transition
   val pretty_setmargin: int -> Toplevel.transition -> Toplevel.transition
   val print_context: Toplevel.transition -> Toplevel.transition
   val print_theory: Toplevel.transition -> Toplevel.transition
@@ -152,8 +152,8 @@
 
 (* use ML text *)
 
-fun use name = Toplevel.keep (fn state =>
-  Context.setmp (try Toplevel.theory_of state) ThyInfo.use name);
+fun use path = Toplevel.keep (fn state =>
+  Context.setmp (try Toplevel.theory_of state) (ThyInfo.load_file false) path);
 
 (*passes changes of theory context*)
 val use_mltext_theory = Toplevel.theory' o Context.use_mltext_theory;
@@ -168,7 +168,7 @@
 
 (* current working directory *)
 
-fun cd dir = Toplevel.imperative (fn () => (File.cd (Path.unpack dir)));
+fun cd path = Toplevel.imperative (fn () => (File.cd path));
 val pwd = Toplevel.imperative (fn () => writeln (Path.pack (File.pwd ())));
 
 
@@ -184,11 +184,11 @@
 (* present draft files *)
 
 fun display_drafts files = Toplevel.imperative (fn () =>
-  let val outfile = File.quote_sysify_path (Present.drafts "dvi" (map Path.unpack files))
+  let val outfile = File.quote_sysify_path (Present.drafts "dvi" files)
   in system ("\"$ISATOOL\" display -c " ^ outfile ^ " &"); () end);
 
 fun print_drafts files = Toplevel.imperative (fn () =>
-  let val outfile = File.quote_sysify_path (Present.drafts "ps" (map Path.unpack files))
+  let val outfile = File.quote_sysify_path (Present.drafts "ps" files)
   in system ("\"$ISATOOL\" print -c " ^ outfile); () end);
 
 
diff -r 5f5605361aad -r e22fad2b6f6f src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Jun 15 13:23:39 2004 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Jun 15 13:24:02 2004 +0200
@@ -237,7 +237,7 @@
 
 val useP =
   OuterSyntax.command "use" "eval ML text from file" K.diag
-    (P.name >> (Toplevel.no_timing oo IsarCmd.use));
+    (P.path >> (Toplevel.no_timing oo IsarCmd.use));
 
 val mlP =
   OuterSyntax.command "ML" "eval ML text (diagnostic)" K.diag
@@ -661,7 +661,7 @@
 
 val cdP =
   OuterSyntax.improper_command "cd" "change current working directory" K.diag
-    (P.name >> (Toplevel.no_timing oo IsarCmd.cd));
+    (P.path >> (Toplevel.no_timing oo IsarCmd.cd));
 
 val pwdP =
   OuterSyntax.improper_command "pwd" "print current working directory" K.diag
@@ -705,11 +705,11 @@
 
 val display_draftsP =
   OuterSyntax.improper_command "display_drafts" "display raw source files with symbols"
-    K.diag (Scan.repeat1 P.name >> (Toplevel.no_timing oo IsarCmd.display_drafts));
+    K.diag (Scan.repeat1 P.path >> (Toplevel.no_timing oo IsarCmd.display_drafts));
 
 val print_draftsP =
   OuterSyntax.improper_command "print_drafts" "print raw source files with symbols"
-    K.diag (Scan.repeat1 P.name >> (Toplevel.no_timing oo IsarCmd.print_drafts));
+    K.diag (Scan.repeat1 P.path >> (Toplevel.no_timing oo IsarCmd.print_drafts));
 
 val opt_limits =
   Scan.option P.nat -- Scan.option (P.$$$ "," |-- P.!!! P.nat);