added ML antiquotation @{path};
authorwenzelm
Thu Mar 13 11:34:05 2014 +0100 (2014-03-13)
changeset 56135efa24d31e595
parent 56134 4a7a07c01857
child 56136 81c66d9e274b
added ML antiquotation @{path};
NEWS
src/Doc/antiquote_setup.ML
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/Pure/Thy/thy_load.ML
src/Tools/WWW_Find/unicode_symbols.ML
     1.1 --- a/NEWS	Thu Mar 13 10:34:48 2014 +0100
     1.2 +++ b/NEWS	Thu Mar 13 11:34:05 2014 +0100
     1.3 @@ -445,6 +445,12 @@
     1.4  * ML antiquotation @{here} refers to its source position, which is
     1.5  occasionally useful for experimentation and diagnostic purposes.
     1.6  
     1.7 +* ML antiquotation @{path} produces a Path.T value, similarly to
     1.8 +Path.explode, but with compile-time check against the file-system and
     1.9 +some PIDE markup.  Note that unlike theory source, ML does not have a
    1.10 +well-defined master directory, so an absolute symbolic path
    1.11 +specification is usually required, e.g. "~~/src/HOL".
    1.12 +
    1.13  
    1.14  *** System ***
    1.15  
     2.1 --- a/src/Doc/antiquote_setup.ML	Thu Mar 13 10:34:48 2014 +0100
     2.2 +++ b/src/Doc/antiquote_setup.ML	Thu Mar 13 11:34:05 2014 +0100
     2.3 @@ -166,12 +166,12 @@
     2.4    | parse_named _ _ = [];
     2.5  
     2.6  val jedit_actions =
     2.7 -  (case XML.parse (File.read (Path.explode "~~/src/Tools/jEdit/src/actions.xml")) of
     2.8 +  (case XML.parse (File.read @{path "~~/src/Tools/jEdit/src/actions.xml"}) of
     2.9      XML.Elem (("ACTIONS", _), body) => maps (parse_named "ACTION") body
    2.10    | _ => []);
    2.11  
    2.12  val jedit_dockables =
    2.13 -  (case XML.parse (File.read (Path.explode "~~/src/Tools/jEdit/src/dockables.xml")) of
    2.14 +  (case XML.parse (File.read @{path "~~/src/Tools/jEdit/src/dockables.xml"}) of
    2.15      XML.Elem (("DOCKABLES", _), body) => maps (parse_named "DOCKABLE") body
    2.16    | _ => []);
    2.17  
     3.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Mar 13 10:34:48 2014 +0100
     3.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Mar 13 11:34:05 2014 +0100
     3.3 @@ -200,10 +200,10 @@
     3.4  (** invocation of Haskell interpreter **)
     3.5  
     3.6  val narrowing_engine =
     3.7 -  File.read (Path.explode "~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs")
     3.8 +  File.read @{path "~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs"}
     3.9  
    3.10  val pnf_narrowing_engine =
    3.11 -  File.read (Path.explode "~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs")
    3.12 +  File.read @{path "~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs"}
    3.13  
    3.14  fun exec verbose code =
    3.15    ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") verbose code)
     4.1 --- a/src/Pure/Thy/thy_load.ML	Thu Mar 13 10:34:48 2014 +0100
     4.2 +++ b/src/Pure/Thy/thy_load.ML	Thu Mar 13 11:34:05 2014 +0100
     4.3 @@ -190,13 +190,14 @@
     4.4    in (thy, present, size text) end;
     4.5  
     4.6  
     4.7 -(* document antiquotation *)
     4.8 +(* antiquotations *)
     4.9  
    4.10 -fun file_antiq strict ctxt (name, pos) =
    4.11 +local
    4.12 +
    4.13 +fun check_path strict ctxt dir (name, pos) =
    4.14    let
    4.15      val _ = Context_Position.report ctxt pos Markup.language_path;
    4.16  
    4.17 -    val dir = master_directory (Proof_Context.theory_of ctxt);
    4.18      val path = Path.append dir (Path.explode name)
    4.19        handle ERROR msg => error (msg ^ Position.here pos);
    4.20  
    4.21 @@ -213,16 +214,30 @@
    4.22              Context_Position.if_visible ctxt Output.report
    4.23                (Markup.markup (Markup.bad |> Markup.properties (Position.properties_of pos)) msg)
    4.24          end;
    4.25 +  in path end;
    4.26 +
    4.27 +fun file_antiq strict ctxt (name, pos) =
    4.28 +  let
    4.29 +    val dir = master_directory (Proof_Context.theory_of ctxt);
    4.30 +    val _ = check_path strict ctxt dir (name, pos);
    4.31    in
    4.32      space_explode "/" name
    4.33      |> map Thy_Output.verb_text
    4.34      |> space_implode (Thy_Output.verb_text "/" ^ "\\discretionary{}{}{}")
    4.35    end;
    4.36  
    4.37 +in
    4.38 +
    4.39  val _ = Theory.setup
    4.40 -  (Thy_Output.antiquotation (Binding.name "file") (Scan.lift (Parse.position Parse.path))
    4.41 + (Thy_Output.antiquotation (Binding.name "file") (Scan.lift (Parse.position Parse.path))
    4.42      (file_antiq true o #context) #>
    4.43 -  (Thy_Output.antiquotation (Binding.name "file_unchecked") (Scan.lift (Parse.position Parse.path))
    4.44 -    (file_antiq false o #context)));
    4.45 +  Thy_Output.antiquotation (Binding.name "file_unchecked") (Scan.lift (Parse.position Parse.path))
    4.46 +    (file_antiq false o #context) #>
    4.47 +  ML_Antiquotation.value (Binding.name "path")
    4.48 +    (Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, arg) =>
    4.49 +      let val path = check_path true ctxt Path.current arg
    4.50 +      in "Path.explode " ^ ML_Syntax.print_string (Path.implode path) end)));
    4.51  
    4.52  end;
    4.53 +
    4.54 +end;
     5.1 --- a/src/Tools/WWW_Find/unicode_symbols.ML	Thu Mar 13 10:34:48 2014 +0100
     5.2 +++ b/src/Tools/WWW_Find/unicode_symbols.ML	Thu Mar 13 11:34:05 2014 +0100
     5.3 @@ -177,7 +177,7 @@
     5.4  
     5.5  local
     5.6  val (fromsym, fromabbr, tosym, toabbr) =
     5.7 -  read_symbols (Path.explode "~~/src/Tools/WWW_Find/etc/symbols");
     5.8 +  read_symbols @{path "~~/src/Tools/WWW_Find/etc/symbols"};
     5.9  in
    5.10  val symbol_to_unicode = Symtab.lookup fromsym;
    5.11  val abbrev_to_unicode = Symtab.lookup fromabbr;