clarified error;
authorwenzelm
Fri Aug 12 13:34:59 2016 +0200 (2016-08-12 ago)
changeset 636732314e99c18a7
parent 63672 5a7c919a4ada
child 63674 f97f2ad2486a
clarified error;
src/Pure/PIDE/resources.ML
     1.1 --- a/src/Pure/PIDE/resources.ML	Fri Aug 12 13:16:04 2016 +0200
     1.2 +++ b/src/Pure/PIDE/resources.ML	Fri Aug 12 13:34:59 2016 +0200
     1.3 @@ -220,8 +220,10 @@
     1.4    Thy_Output.antiquotation @{binding dir} (Scan.lift (Parse.position Parse.path))
     1.5      (path_antiq (SOME File.check_dir) o #context) #>
     1.6    ML_Antiquotation.value @{binding file}
     1.7 -    (Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, arg) =>
     1.8 -      let val path = check_path ctxt Path.current arg |> File.check_file
     1.9 +    (Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, (name, pos)) =>
    1.10 +      let
    1.11 +        val path = check_path ctxt Path.current (name, pos);
    1.12 +        val _ = File.check_file path handle ERROR msg => err msg pos;
    1.13        in "Path.explode " ^ ML_Syntax.print_string (Path.implode path) end)));
    1.14  
    1.15  end;