src/Pure/Thy/thy_load.ML
changeset 54705 0dff3326d12a
parent 54526 92961f196d9e
child 55614 e2d71b8b0d95
     1.1 --- a/src/Pure/Thy/thy_load.ML	Mon Dec 09 12:27:18 2013 +0100
     1.2 +++ b/src/Pure/Thy/thy_load.ML	Mon Dec 09 20:16:12 2013 +0100
     1.3 @@ -192,20 +192,24 @@
     1.4  
     1.5  (* document antiquotation *)
     1.6  
     1.7 +fun file_antiq do_check ctxt (name, pos) =
     1.8 +  let
     1.9 +    val dir = master_directory (Proof_Context.theory_of ctxt);
    1.10 +    val path = Path.append dir (Path.explode name);
    1.11 +    val _ =
    1.12 +      if not do_check orelse File.exists path then ()
    1.13 +      else error ("Bad file: " ^ Path.print (Path.expand path) ^ Position.here pos);
    1.14 +    val _ = Position.report pos (Markup.path name);
    1.15 +  in
    1.16 +    space_explode "/" name
    1.17 +    |> map Thy_Output.verb_text
    1.18 +    |> space_implode (Thy_Output.verb_text "/" ^ "\\discretionary{}{}{}")
    1.19 +  end;
    1.20 +
    1.21  val _ = Theory.setup
    1.22    (Thy_Output.antiquotation (Binding.name "file") (Scan.lift (Parse.position Parse.path))
    1.23 -    (fn {context = ctxt, ...} => fn (name, pos) =>
    1.24 -      let
    1.25 -        val dir = master_directory (Proof_Context.theory_of ctxt);
    1.26 -        val path = Path.append dir (Path.explode name);
    1.27 -        val _ =
    1.28 -          if File.exists path then ()
    1.29 -          else error ("Bad file: " ^ Path.print (Path.expand path) ^ Position.here pos);
    1.30 -        val _ = Position.report pos (Markup.path name);
    1.31 -      in
    1.32 -        space_explode "/" name
    1.33 -        |> map Thy_Output.verb_text
    1.34 -        |> space_implode (Thy_Output.verb_text "/" ^ "\\discretionary{}{}{}")
    1.35 -      end));
    1.36 +    (file_antiq true o #context) #>
    1.37 +  (Thy_Output.antiquotation (Binding.name "file_unchecked") (Scan.lift (Parse.position Parse.path))
    1.38 +    (file_antiq false o #context)));
    1.39  
    1.40  end;