clarified Parse.path vs. Parse.explode -- prefer errors in proper transaction context;

--- a/src/HOL/Import/import_rule.ML	Wed Aug 22 12:17:55 2012 +0200
+++ b/src/HOL/Import/import_rule.ML	Wed Aug 22 12:47:49 2012 +0200
@@ -444,7 +444,8 @@
   (thy, init_state) |> File.fold_lines process_line path |> fst
 
 val _ = Outer_Syntax.command @{command_spec "import_file"}
-  "Import a recorded proof file" (Parse.path >> process_file >> Toplevel.theory)
+  "Import a recorded proof file"
+  (Parse.path >> (fn name => Toplevel.theory (fn thy => process_file (Path.explode name) thy)))
 
 
 end

--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Wed Aug 22 12:17:55 2012 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Wed Aug 22 12:47:49 2012 +0200
@@ -878,10 +878,11 @@
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "import_tptp"} "import TPTP problem"
-    (Parse.path >> (fn path =>
+    (Parse.path >> (fn name =>
       Toplevel.theory (fn thy =>
-       (*NOTE: assumes include files are located at $TPTP/Axioms
-         (which is how TPTP is organised)*)
-       import_file true [Path.dir path, Path.explode "$TPTP"] path [] [] thy)))
+        let val path = Path.explode name
+        (*NOTE: assumes include files are located at $TPTP/Axioms
+          (which is how TPTP is organised)*)
+        in import_file true [Path.dir path, Path.explode "$TPTP"] path [] [] thy end)))
 
 end

--- a/src/Pure/Isar/isar_cmd.ML	Wed Aug 22 12:17:55 2012 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Aug 22 12:47:49 2012 +0200
@@ -40,8 +40,8 @@
   val ml_diag: bool -> Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition
   val diag_state: Proof.context -> Toplevel.state
   val diag_goal: Proof.context -> {context: Proof.context, facts: thm list, goal: thm}
-  val display_drafts: Path.T list -> Toplevel.transition -> Toplevel.transition
-  val print_drafts: Path.T list -> Toplevel.transition -> Toplevel.transition
+  val display_drafts: string list -> Toplevel.transition -> Toplevel.transition
+  val print_drafts: string list -> Toplevel.transition -> Toplevel.transition
   val print_context: Toplevel.transition -> Toplevel.transition
   val print_theory: bool -> Toplevel.transition -> Toplevel.transition
   val print_syntax: Toplevel.transition -> Toplevel.transition
@@ -314,12 +314,16 @@
 
 (* present draft files *)
 
-fun display_drafts files = Toplevel.imperative (fn () =>
-  let val outfile = File.shell_path (Present.drafts (getenv "ISABELLE_DOC_FORMAT") files)
+fun display_drafts names = Toplevel.imperative (fn () =>
+  let
+    val paths = map Path.explode names;
+    val outfile = File.shell_path (Present.drafts (getenv "ISABELLE_DOC_FORMAT") paths);
   in Isabelle_System.isabelle_tool "display" ("-c " ^ outfile ^ " &"); () end);
 
-fun print_drafts files = Toplevel.imperative (fn () =>
-  let val outfile = File.shell_path (Present.drafts "ps" files)
+fun print_drafts names = Toplevel.imperative (fn () =>
+  let
+    val paths = map Path.explode names;
+    val outfile = File.shell_path (Present.drafts "ps" paths);
   in Isabelle_System.isabelle_tool "print" ("-c " ^ outfile); () end);
 
 

--- a/src/Pure/Isar/isar_syn.ML	Wed Aug 22 12:17:55 2012 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Aug 22 12:47:49 2012 +0200
@@ -271,7 +271,8 @@
 
 val _ =
   Outer_Syntax.command @{command_spec "use"} "ML text from file"
-    (Parse.path >> (fn path => Toplevel.generic_theory (Thy_Load.exec_ml path)));
+    (Parse.path >> (fn name =>
+      Toplevel.generic_theory (fn gthy => Thy_Load.exec_ml (Path.explode name) gthy)));
 
 val _ =
   Outer_Syntax.command @{command_spec "ML"} "ML text within theory or local theory"
@@ -923,7 +924,8 @@
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "cd"} "change current working directory"
-    (Parse.path >> (fn path => Toplevel.no_timing o Toplevel.imperative (fn () => File.cd path)));
+    (Parse.path >> (fn name =>
+      Toplevel.no_timing o Toplevel.imperative (fn () => File.cd (Path.explode name))));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "pwd"} "print current working directory"

--- a/src/Pure/Isar/parse.ML	Wed Aug 22 12:17:55 2012 +0200
+++ b/src/Pure/Isar/parse.ML	Wed Aug 22 12:47:49 2012 +0200
@@ -65,7 +65,7 @@
   val binding: binding parser
   val xname: xstring parser
   val text: string parser
-  val path: Path.T parser
+  val path: string parser
   val liberal_name: xstring parser
   val parname: string parser
   val parbinding: binding parser
@@ -250,7 +250,7 @@
 val text = group (fn () => "text")
   (short_ident || long_ident || sym_ident || string || number || verbatim);
 
-val path = group (fn () => "file name/path specification") name >> Path.explode;
+val path = group (fn () => "file name/path specification") name;
 
 val liberal_name = keyword_ident_or_symbolic || xname;
 

--- a/src/Pure/Thy/thy_header.ML	Wed Aug 22 12:17:55 2012 +0200
+++ b/src/Pure/Thy/thy_header.ML	Wed Aug 22 12:47:49 2012 +0200
@@ -84,7 +84,7 @@
 
 local
 
-val file_name = Parse.group (fn () => "file name") Parse.path;
+val file_name = Parse.group (fn () => "file name") Parse.path >> Path.explode;
 val theory_name = Parse.group (fn () => "theory name") Parse.name;
 
 val opt_files =

--- a/src/Pure/Thy/thy_load.ML	Wed Aug 22 12:17:55 2012 +0200
+++ b/src/Pure/Thy/thy_load.ML	Wed Aug 22 12:47:49 2012 +0200
@@ -92,7 +92,9 @@
 
 fun find_file toks =
   rev (clean_tokens toks) |> get_first (fn (i, tok) =>
-    if Token.is_name tok then SOME (i, Path.explode (Token.content_of tok))
+    if Token.is_name tok then
+    SOME (i, Path.explode (Token.content_of tok))
+      handle ERROR msg => error (msg ^ Token.pos_of tok)
     else NONE);
 
 fun command_files path exts =
@@ -126,12 +128,14 @@
   in (dir, files) end;
 
 fun parse_files cmd =
-  Scan.ahead Parse.not_eof -- Parse.path >> (fn (tok, path) => fn thy =>
+  Scan.ahead Parse.not_eof -- Parse.path >> (fn (tok, name) => fn thy =>
     (case Token.get_files tok of
       SOME files => files
     | NONE =>
-        (warning ("Dynamic loading of files: " ^ Path.print path ^ Token.pos_of tok);
-          read_files cmd (master_directory thy) path)));
+        let
+          val path = Path.explode name;
+          val _ = warning ("Dynamic loading of files: " ^ Path.print path);
+        in read_files cmd (master_directory thy) path end));
 
 fun resolve_files dir span =
   (case span of

--- a/src/Pure/pure_syn.ML	Wed Aug 22 12:17:55 2012 +0200
+++ b/src/Pure/pure_syn.ML	Wed Aug 22 12:47:49 2012 +0200
@@ -19,8 +19,9 @@
   Outer_Syntax.command
     (("ML_file", Keyword.tag_ml Keyword.thy_load), Position.none) "ML text from file"
     (Scan.ahead Parse.path -- Thy_Load.parse_files "ML_file"
-      >> (fn (src_path, files) => Toplevel.generic_theory (fn gthy =>
+      >> (fn (name, files) => Toplevel.generic_theory (fn gthy =>
         let
+          val src_path = Path.explode name;
           val (dir, [(txt, pos)]) = files (Context.theory_of gthy);
           val provide = Thy_Load.provide (src_path, (File.full_path dir src_path, SHA1.digest txt));
         in