src/Doc/antiquote_setup.ML
changeset 54705 0dff3326d12a
parent 54372 2d61935eed4a
child 55742 a989bdaf8121
--- a/src/Doc/antiquote_setup.ML	Mon Dec 09 12:27:18 2013 +0100
+++ b/src/Doc/antiquote_setup.ML	Mon Dec 09 20:16:12 2013 +0100
@@ -47,22 +47,6 @@
     (K (split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"));
 
 
-(* unchecked file *)
-
-val file_unchecked_setup =
-  Thy_Output.antiquotation @{binding file_unchecked} (Scan.lift (Parse.position Parse.path))
-    (fn {context = ctxt, ...} => fn (name, pos) =>
-      let
-        val dir = Thy_Load.master_directory (Proof_Context.theory_of ctxt);
-        val path = Path.append dir (Path.explode name);
-        val _ = Position.report pos (Markup.path name);
-      in
-        space_explode "/" name
-        |> map Thy_Output.verb_text
-        |> space_implode (Thy_Output.verb_text "/" ^ "\\discretionary{}{}{}")
-      end);
-
-
 (* ML text *)
 
 local
@@ -249,7 +233,6 @@
 
 val setup =
   verbatim_setup #>
-  file_unchecked_setup #>
   index_ml_setup #>
   named_thms_setup #>
   thy_file_setup #>