tuned;
authorwenzelm
Sat Dec 16 17:23:00 2017 +0100 (17 months ago)
changeset 6721753867014e299
parent 67216 99815211970c
child 67218 e62d72699666
tuned;
src/Pure/PIDE/resources.ML
     1.1 --- a/src/Pure/PIDE/resources.ML	Sat Dec 16 16:57:06 2017 +0100
     1.2 +++ b/src/Pure/PIDE/resources.ML	Sat Dec 16 17:23:00 2017 +0100
     1.3 @@ -197,11 +197,9 @@
     1.4        | SOME ((_, id'), _) => id = id'));
     1.5  
     1.6  
     1.7 -(* antiquotations *)
     1.8 +(* formal check *)
     1.9  
    1.10 -local
    1.11 -
    1.12 -fun gen_check check_file ctxt dir (name, pos) =
    1.13 +fun formal_check check_file ctxt dir (name, pos) =
    1.14    let
    1.15      fun err msg = error (msg ^ Position.here pos);
    1.16  
    1.17 @@ -212,6 +210,15 @@
    1.18      val _ = check_file path handle ERROR msg => err msg;
    1.19    in path end;
    1.20  
    1.21 +val check_path = formal_check I;
    1.22 +val check_file = formal_check File.check_file;
    1.23 +val check_dir = formal_check File.check_dir;
    1.24 +
    1.25 +
    1.26 +(* antiquotations *)
    1.27 +
    1.28 +local
    1.29 +
    1.30  fun document_antiq check ctxt (name, pos) =
    1.31    let
    1.32      val dir = master_directory (Proof_Context.theory_of ctxt);
    1.33 @@ -229,10 +236,6 @@
    1.34  
    1.35  in
    1.36  
    1.37 -val check_path = gen_check I;
    1.38 -val check_file = gen_check File.check_file;
    1.39 -val check_dir = gen_check File.check_dir;
    1.40 -
    1.41  val _ = Theory.setup
    1.42   (Thy_Output.antiquotation \<^binding>\<open>path\<close> (Scan.lift (Parse.position Parse.path))
    1.43      (document_antiq check_path o #context) #>