src/Pure/PIDE/resources.ML
changeset 63669 256fc20716f2
parent 61381 ddca85598c65
child 63673 2314e99c18a7
     1.1 --- a/src/Pure/PIDE/resources.ML	Thu Aug 11 18:26:16 2016 +0200
     1.2 +++ b/src/Pure/PIDE/resources.ML	Thu Aug 11 18:26:44 2016 +0200
     1.3 @@ -184,33 +184,25 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun check_path strict ctxt dir (name, pos) =
     1.8 +fun err msg pos = error (msg ^ Position.here pos);
     1.9 +
    1.10 +fun check_path ctxt dir (name, pos) =
    1.11    let
    1.12      val _ = Context_Position.report ctxt pos Markup.language_path;
    1.13  
    1.14 -    val path = Path.append dir (Path.explode name)
    1.15 -      handle ERROR msg => error (msg ^ Position.here pos);
    1.16 -
    1.17 +    val path = Path.append dir (Path.explode name) handle ERROR msg => err msg pos;
    1.18 +    val _ = Path.expand path handle ERROR msg => err msg pos;
    1.19      val _ = Context_Position.report ctxt pos (Markup.path (Path.smart_implode path));
    1.20 -    val _ =
    1.21 -      if can Path.expand path andalso File.exists path then ()
    1.22 -      else
    1.23 -        let
    1.24 -          val path' = perhaps (try Path.expand) path;
    1.25 -          val msg = "Bad file: " ^ Path.print path' ^ Position.here pos;
    1.26 -        in
    1.27 -          if strict then error msg
    1.28 -          else if Context_Position.is_visible ctxt then
    1.29 -            Output.report
    1.30 -              [Markup.markup (Markup.bad |> Markup.properties (Position.properties_of pos)) msg]
    1.31 -          else ()
    1.32 -        end;
    1.33    in path end;
    1.34  
    1.35 -fun file_antiq strict ctxt (name, pos) =
    1.36 +fun path_antiq check_file ctxt (name, pos) =
    1.37    let
    1.38      val dir = master_directory (Proof_Context.theory_of ctxt);
    1.39 -    val _ = check_path strict ctxt dir (name, pos);
    1.40 +    val path = check_path ctxt dir (name, pos);
    1.41 +    val _ =
    1.42 +      (case check_file of
    1.43 +        NONE => path
    1.44 +      | SOME check => (check path handle ERROR msg => err msg pos));
    1.45    in
    1.46      space_explode "/" name
    1.47      |> map Latex.output_ascii
    1.48 @@ -221,13 +213,15 @@
    1.49  in
    1.50  
    1.51  val _ = Theory.setup
    1.52 - (Thy_Output.antiquotation @{binding file} (Scan.lift (Parse.position Parse.path))
    1.53 -    (file_antiq true o #context) #>
    1.54 -  Thy_Output.antiquotation @{binding file_unchecked} (Scan.lift (Parse.position Parse.path))
    1.55 -    (file_antiq false o #context) #>
    1.56 -  ML_Antiquotation.value @{binding path}
    1.57 + (Thy_Output.antiquotation @{binding path} (Scan.lift (Parse.position Parse.path))
    1.58 +    (path_antiq NONE o #context) #>
    1.59 +  Thy_Output.antiquotation @{binding file} (Scan.lift (Parse.position Parse.path))
    1.60 +    (path_antiq (SOME File.check_file) o #context) #>
    1.61 +  Thy_Output.antiquotation @{binding dir} (Scan.lift (Parse.position Parse.path))
    1.62 +    (path_antiq (SOME File.check_dir) o #context) #>
    1.63 +  ML_Antiquotation.value @{binding file}
    1.64      (Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, arg) =>
    1.65 -      let val path = check_path true ctxt Path.current arg
    1.66 +      let val path = check_path ctxt Path.current arg |> File.check_file
    1.67        in "Path.explode " ^ ML_Syntax.print_string (Path.implode path) end)));
    1.68  
    1.69  end;