src/Pure/PIDE/resources.ML
changeset 63675 e217525d6b64
parent 63673 2314e99c18a7
child 65058 3e9f382fb67e
     1.1 --- a/src/Pure/PIDE/resources.ML	Fri Aug 12 14:02:48 2016 +0200
     1.2 +++ b/src/Pure/PIDE/resources.ML	Fri Aug 12 14:19:27 2016 +0200
     1.3 @@ -186,23 +186,23 @@
     1.4  
     1.5  fun err msg pos = error (msg ^ Position.here pos);
     1.6  
     1.7 -fun check_path ctxt dir (name, pos) =
     1.8 +fun check_path check_file ctxt dir (name, pos) =
     1.9    let
    1.10      val _ = Context_Position.report ctxt pos Markup.language_path;
    1.11  
    1.12      val path = Path.append dir (Path.explode name) handle ERROR msg => err msg pos;
    1.13      val _ = Path.expand path handle ERROR msg => err msg pos;
    1.14      val _ = Context_Position.report ctxt pos (Markup.path (Path.smart_implode path));
    1.15 -  in path end;
    1.16 -
    1.17 -fun path_antiq check_file ctxt (name, pos) =
    1.18 -  let
    1.19 -    val dir = master_directory (Proof_Context.theory_of ctxt);
    1.20 -    val path = check_path ctxt dir (name, pos);
    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 +  in path end;
    1.26 +
    1.27 +fun document_antiq check_file ctxt (name, pos) =
    1.28 +  let
    1.29 +    val dir = master_directory (Proof_Context.theory_of ctxt);
    1.30 +    val _ = check_path check_file ctxt dir (name, pos);
    1.31    in
    1.32      space_explode "/" name
    1.33      |> map Latex.output_ascii
    1.34 @@ -210,21 +210,28 @@
    1.35      |> enclose "\\isatt{" "}"
    1.36    end;
    1.37  
    1.38 +fun ML_antiq check_file ctxt (name, pos) =
    1.39 +  let val path = check_path check_file ctxt Path.current (name, pos);
    1.40 +  in "Path.explode " ^ ML_Syntax.print_string (Path.implode path) end;
    1.41 +
    1.42  in
    1.43  
    1.44  val _ = Theory.setup
    1.45   (Thy_Output.antiquotation @{binding path} (Scan.lift (Parse.position Parse.path))
    1.46 -    (path_antiq NONE o #context) #>
    1.47 +    (document_antiq NONE o #context) #>
    1.48    Thy_Output.antiquotation @{binding file} (Scan.lift (Parse.position Parse.path))
    1.49 -    (path_antiq (SOME File.check_file) o #context) #>
    1.50 +    (document_antiq (SOME File.check_file) o #context) #>
    1.51    Thy_Output.antiquotation @{binding dir} (Scan.lift (Parse.position Parse.path))
    1.52 -    (path_antiq (SOME File.check_dir) o #context) #>
    1.53 +    (document_antiq (SOME File.check_dir) o #context) #>
    1.54 +  ML_Antiquotation.value @{binding path}
    1.55 +    (Args.context -- Scan.lift (Parse.position Parse.path)
    1.56 +      >> uncurry (ML_antiq NONE)) #>
    1.57    ML_Antiquotation.value @{binding file}
    1.58 -    (Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, (name, pos)) =>
    1.59 -      let
    1.60 -        val path = check_path ctxt Path.current (name, pos);
    1.61 -        val _ = File.check_file path handle ERROR msg => err msg pos;
    1.62 -      in "Path.explode " ^ ML_Syntax.print_string (Path.implode path) end)));
    1.63 +    (Args.context -- Scan.lift (Parse.position Parse.path)
    1.64 +      >> uncurry (ML_antiq (SOME File.check_file))) #>
    1.65 +  ML_Antiquotation.value @{binding dir}
    1.66 +    (Args.context -- Scan.lift (Parse.position Parse.path)
    1.67 +      >> uncurry (ML_antiq (SOME File.check_dir))));
    1.68  
    1.69  end;
    1.70