clarified signature;
authorwenzelm
Sat Dec 16 12:27:10 2017 +0100 (17 months ago)
changeset 67209fca5f2988091
parent 67208 16519cd83ed4
child 67210 f80bdbe76934
clarified signature;
src/Pure/PIDE/resources.ML
     1.1 --- a/src/Pure/PIDE/resources.ML	Sat Dec 16 12:16:40 2017 +0100
     1.2 +++ b/src/Pure/PIDE/resources.ML	Sat Dec 16 12:27:10 2017 +0100
     1.3 @@ -28,6 +28,9 @@
     1.4    val provide: Path.T * SHA1.digest -> theory -> theory
     1.5    val provide_parse_files: string -> (theory -> Token.file list * theory) parser
     1.6    val loaded_files_current: theory -> bool
     1.7 +  val check_path: Proof.context -> Path.T -> string * Position.T -> Path.T
     1.8 +  val check_file: Proof.context -> Path.T -> string * Position.T -> Path.T
     1.9 +  val check_dir: Proof.context -> Path.T -> string * Position.T -> Path.T
    1.10  end;
    1.11  
    1.12  structure Resources: RESOURCES =
    1.13 @@ -198,7 +201,7 @@
    1.14  
    1.15  fun err msg pos = error (msg ^ Position.here pos);
    1.16  
    1.17 -fun check_path check_file ctxt dir (name, pos) =
    1.18 +fun gen_check_path check_file ctxt dir (name, pos) =
    1.19    let
    1.20      val _ = Context_Position.report ctxt pos Markup.language_path;
    1.21  
    1.22 @@ -211,10 +214,10 @@
    1.23        | SOME check => (check path handle ERROR msg => err msg pos));
    1.24    in path end;
    1.25  
    1.26 -fun document_antiq check_file ctxt (name, pos) =
    1.27 +fun document_antiq check 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 +    val _ = check ctxt dir (name, pos);
    1.32    in
    1.33      space_explode "/" name
    1.34      |> map Latex.output_ascii
    1.35 @@ -222,28 +225,29 @@
    1.36      |> enclose "\\isatt{" "}"
    1.37    end;
    1.38  
    1.39 -fun ML_antiq check_file ctxt (name, pos) =
    1.40 -  let val path = check_path check_file ctxt Path.current (name, pos);
    1.41 +fun ML_antiq check ctxt (name, pos) =
    1.42 +  let val path = check ctxt Path.current (name, pos);
    1.43    in "Path.explode " ^ ML_Syntax.print_string (Path.implode path) end;
    1.44  
    1.45  in
    1.46  
    1.47 +val check_path = gen_check_path NONE;
    1.48 +val check_file = gen_check_path (SOME File.check_file);
    1.49 +val check_dir = gen_check_path (SOME File.check_dir);
    1.50 +
    1.51  val _ = Theory.setup
    1.52   (Thy_Output.antiquotation \<^binding>\<open>path\<close> (Scan.lift (Parse.position Parse.path))
    1.53 -    (document_antiq NONE o #context) #>
    1.54 +    (document_antiq check_path o #context) #>
    1.55    Thy_Output.antiquotation \<^binding>\<open>file\<close> (Scan.lift (Parse.position Parse.path))
    1.56 -    (document_antiq (SOME File.check_file) o #context) #>
    1.57 +    (document_antiq check_file o #context) #>
    1.58    Thy_Output.antiquotation \<^binding>\<open>dir\<close> (Scan.lift (Parse.position Parse.path))
    1.59 -    (document_antiq (SOME File.check_dir) o #context) #>
    1.60 +    (document_antiq check_dir o #context) #>
    1.61    ML_Antiquotation.value \<^binding>\<open>path\<close>
    1.62 -    (Args.context -- Scan.lift (Parse.position Parse.path)
    1.63 -      >> uncurry (ML_antiq NONE)) #>
    1.64 +    (Args.context -- Scan.lift (Parse.position Parse.path) >> uncurry (ML_antiq check_path)) #>
    1.65    ML_Antiquotation.value \<^binding>\<open>file\<close>
    1.66 -    (Args.context -- Scan.lift (Parse.position Parse.path)
    1.67 -      >> uncurry (ML_antiq (SOME File.check_file))) #>
    1.68 +    (Args.context -- Scan.lift (Parse.position Parse.path) >> uncurry (ML_antiq check_file)) #>
    1.69    ML_Antiquotation.value \<^binding>\<open>dir\<close>
    1.70 -    (Args.context -- Scan.lift (Parse.position Parse.path)
    1.71 -      >> uncurry (ML_antiq (SOME File.check_dir))));
    1.72 +    (Args.context -- Scan.lift (Parse.position Parse.path) >> uncurry (ML_antiq check_dir)));
    1.73  
    1.74  end;
    1.75