# HG changeset patch # User wenzelm # Date 1345632469 -7200 # Node ID 46e053eda5ddda011c98df703c2ee2df8c85ade8 # Parent 03232f0bb5c4f387654ff52f59e403dca986ffa4 clarified Parse.path vs. Parse.explode -- prefer errors in proper transaction context; diff -r 03232f0bb5c4 -r 46e053eda5dd src/HOL/Import/import_rule.ML --- 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 diff -r 03232f0bb5c4 -r 46e053eda5dd src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML --- 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 diff -r 03232f0bb5c4 -r 46e053eda5dd src/Pure/Isar/isar_cmd.ML --- 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); diff -r 03232f0bb5c4 -r 46e053eda5dd src/Pure/Isar/isar_syn.ML --- 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" diff -r 03232f0bb5c4 -r 46e053eda5dd src/Pure/Isar/parse.ML --- 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; diff -r 03232f0bb5c4 -r 46e053eda5dd src/Pure/Thy/thy_header.ML --- 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 = diff -r 03232f0bb5c4 -r 46e053eda5dd src/Pure/Thy/thy_load.ML --- 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 diff -r 03232f0bb5c4 -r 46e053eda5dd src/Pure/pure_syn.ML --- 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