src/Pure/PIDE/resources.ML
changeset 69286 599b6d0d199b
parent 69243 d98cfb369cbd
child 69287 94fa3376ba33
     1.1 --- a/src/Pure/PIDE/resources.ML	Sat Nov 10 17:12:09 2018 +0100
     1.2 +++ b/src/Pure/PIDE/resources.ML	Sat Nov 10 19:01:20 2018 +0100
     1.3 @@ -259,19 +259,20 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun document_antiq check ctxt (name, pos) =
     1.8 -  let
     1.9 -    val dir = master_directory (Proof_Context.theory_of ctxt);
    1.10 -    val _ = check ctxt dir (name, pos);
    1.11 -    val latex =
    1.12 -      space_explode "/" name
    1.13 -      |> map Latex.output_ascii
    1.14 -      |> space_implode (Latex.output_ascii "/" ^ "\\discretionary{}{}{}");
    1.15 -  in Latex.enclose_block "\\isatt{" "}" [Latex.string latex] end;
    1.16 +fun document_antiq check =
    1.17 +  Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, (name, pos)) =>
    1.18 +    let
    1.19 +      val dir = master_directory (Proof_Context.theory_of ctxt);
    1.20 +      val _: Path.T = check ctxt dir (name, pos);
    1.21 +      val latex =
    1.22 +        space_explode "/" name
    1.23 +        |> map Latex.output_ascii
    1.24 +        |> space_implode (Latex.output_ascii "/" ^ "\\discretionary{}{}{}");
    1.25 +    in Latex.enclose_block "\\isatt{" "}" [Latex.string latex] end);
    1.26  
    1.27 -fun ML_antiq check ctxt (name, pos) =
    1.28 -  let val path = check ctxt Path.current (name, pos);
    1.29 -  in "Path.explode " ^ ML_Syntax.print_string (Path.implode path) end;
    1.30 +fun ML_antiq check =
    1.31 +  Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, (name, pos)) =>
    1.32 +    check ctxt Path.current (name, pos) |> ML_Syntax.print_path);
    1.33  
    1.34  in
    1.35  
    1.36 @@ -280,18 +281,12 @@
    1.37      (Scan.lift (Parse.position Parse.embedded)) check_session #>
    1.38    Thy_Output.antiquotation_verbatim \<^binding>\<open>doc\<close>
    1.39      (Scan.lift (Parse.position Parse.embedded)) check_doc #>
    1.40 -  Thy_Output.antiquotation_raw \<^binding>\<open>path\<close>
    1.41 -    (Scan.lift (Parse.position Parse.path)) (document_antiq check_path) #>
    1.42 -  Thy_Output.antiquotation_raw \<^binding>\<open>file\<close>
    1.43 -    (Scan.lift (Parse.position Parse.path)) (document_antiq check_file) #>
    1.44 -  Thy_Output.antiquotation_raw \<^binding>\<open>dir\<close>
    1.45 -    (Scan.lift (Parse.position Parse.path)) (document_antiq check_dir) #>
    1.46 -  ML_Antiquotation.value \<^binding>\<open>path\<close>
    1.47 -    (Args.context -- Scan.lift (Parse.position Parse.path) >> uncurry (ML_antiq check_path)) #>
    1.48 -  ML_Antiquotation.value \<^binding>\<open>file\<close>
    1.49 -    (Args.context -- Scan.lift (Parse.position Parse.path) >> uncurry (ML_antiq check_file)) #>
    1.50 -  ML_Antiquotation.value \<^binding>\<open>dir\<close>
    1.51 -    (Args.context -- Scan.lift (Parse.position Parse.path) >> uncurry (ML_antiq check_dir)));
    1.52 +  Thy_Output.antiquotation_raw \<^binding>\<open>path\<close> (document_antiq check_path) (K I) #>
    1.53 +  Thy_Output.antiquotation_raw \<^binding>\<open>file\<close> (document_antiq check_file) (K I) #>
    1.54 +  Thy_Output.antiquotation_raw \<^binding>\<open>dir\<close> (document_antiq check_dir) (K I) #>
    1.55 +  ML_Antiquotation.value \<^binding>\<open>path\<close> (ML_antiq check_path) #>
    1.56 +  ML_Antiquotation.value \<^binding>\<open>file\<close> (ML_antiq check_file) #>
    1.57 +  ML_Antiquotation.value \<^binding>\<open>dir\<close> (ML_antiq check_dir));
    1.58  
    1.59  end;
    1.60