tuned;
authorwenzelm
Sat Dec 16 15:15:51 2017 +0100 (17 months ago)
changeset 6721487038a574d09
parent 67213 01576aebc398
child 67215 03d0c958d65a
tuned;
src/Pure/PIDE/resources.ML
     1.1 --- a/src/Pure/PIDE/resources.ML	Sat Dec 16 15:11:19 2017 +0100
     1.2 +++ b/src/Pure/PIDE/resources.ML	Sat Dec 16 15:15:51 2017 +0100
     1.3 @@ -199,19 +199,15 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun err msg pos = error (msg ^ Position.here pos);
     1.8 -
     1.9 -fun gen_check_path check_file ctxt dir (name, pos) =
    1.10 +fun gen_check check_file ctxt dir (name, pos) =
    1.11    let
    1.12 -    val _ = Context_Position.report ctxt pos Markup.language_path;
    1.13 +    fun err msg = error (msg ^ Position.here pos);
    1.14  
    1.15 -    val path = Path.append dir (Path.explode name) handle ERROR msg => err msg pos;
    1.16 -    val _ = Path.expand path handle ERROR msg => err msg pos;
    1.17 +    val _ = Context_Position.report ctxt pos Markup.language_path;
    1.18 +    val path = Path.append dir (Path.explode name) handle ERROR msg => err msg;
    1.19 +    val _ = Path.expand path handle ERROR msg => err msg;
    1.20      val _ = Context_Position.report ctxt pos (Markup.path (Path.smart_implode path));
    1.21 -    val _ =
    1.22 -      (case check_file of
    1.23 -        NONE => path
    1.24 -      | SOME check => (check path handle ERROR msg => err msg pos));
    1.25 +    val _ = check_file path handle ERROR msg => err msg;
    1.26    in path end;
    1.27  
    1.28  fun document_antiq check ctxt (name, pos) =
    1.29 @@ -231,9 +227,9 @@
    1.30  
    1.31  in
    1.32  
    1.33 -val check_path = gen_check_path NONE;
    1.34 -val check_file = gen_check_path (SOME File.check_file);
    1.35 -val check_dir = gen_check_path (SOME File.check_dir);
    1.36 +val check_path = gen_check I;
    1.37 +val check_file = gen_check File.check_file;
    1.38 +val check_dir = gen_check File.check_dir;
    1.39  
    1.40  val _ = Theory.setup
    1.41   (Thy_Output.antiquotation \<^binding>\<open>path\<close> (Scan.lift (Parse.position Parse.path))