more PIDE markup;
authorwenzelm
Fri Sep 01 12:47:23 2017 +0200 (2017-09-01)
changeset 66586e5e56c330976
parent 66585 75c090d0e699
child 66587 bfabccdad18e
more PIDE markup;
src/Tools/Code/code_target.ML
     1.1 --- a/src/Tools/Code/code_target.ML	Fri Sep 01 12:19:40 2017 +0200
     1.2 +++ b/src/Tools/Code/code_target.ML	Fri Sep 01 12:47:23 2017 +0200
     1.3 @@ -436,8 +436,14 @@
     1.4  
     1.5  (* code generation *)
     1.6  
     1.7 -fun prep_destination "" = NONE
     1.8 -  | prep_destination s = SOME (Path.explode s);
     1.9 +fun prep_destination (s, pos) =
    1.10 +  if s = "" then NONE
    1.11 +  else
    1.12 +    let
    1.13 +      val _ = Position.report pos Markup.language_path;
    1.14 +      val path = Path.explode s;
    1.15 +      val _ = Position.report pos (Markup.path (Path.smart_implode path));
    1.16 +    in SOME path end;
    1.17  
    1.18  fun export_code ctxt all_public cs seris =
    1.19    let
    1.20 @@ -630,7 +636,7 @@
    1.21  fun code_expr_inP all_public raw_cs =
    1.22    Scan.repeat (@{keyword "in"} |-- Parse.!!! (Parse.name
    1.23      -- Scan.optional (@{keyword "module_name"} |-- Parse.name) ""
    1.24 -    -- Scan.optional (@{keyword "file"} |-- Parse.name) ""
    1.25 +    -- Scan.optional (@{keyword "file"} |-- Parse.position Parse.path) ("", Position.none)
    1.26      -- code_expr_argsP))
    1.27        >> (fn seri_args => export_code_cmd all_public raw_cs seri_args);
    1.28