proper PIDE positions;
authorwenzelm
Wed May 16 23:13:33 2018 +0200 (3 months ago)
changeset 68199f551dd2178ab
parent 68198 6710167e17af
child 68200 5859c688102a
proper PIDE positions;
src/Pure/Thy/export_theory.ML
     1.1 --- a/src/Pure/Thy/export_theory.ML	Wed May 16 21:36:59 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Wed May 16 23:13:33 2018 +0200
     1.3 @@ -6,7 +6,6 @@
     1.4  
     1.5  signature EXPORT_THEORY =
     1.6  sig
     1.7 -  val entity_markup: Name_Space.T -> string -> Markup.T
     1.8  end;
     1.9  
    1.10  structure Export_Theory: EXPORT_THEORY =
    1.11 @@ -14,27 +13,29 @@
    1.12  
    1.13  (* name space entries *)
    1.14  
    1.15 -fun entity_markup space name =
    1.16 +fun entity_markup adjust_pos space name =
    1.17    let
    1.18      val {serial, pos, ...} = Name_Space.the_entry space name;
    1.19 -    val props = Markup.serial_properties serial @ Position.offset_properties_of pos;
    1.20 +    val props = Markup.serial_properties serial @ Position.offset_properties_of (adjust_pos pos);
    1.21    in (Markup.entityN, (Markup.nameN, name) :: props) end;
    1.22  
    1.23 -fun export_decls export_decl parents thy space decls =
    1.24 +fun export_decls export_decl parents thy adjust_pos space decls =
    1.25    (decls, []) |-> fold (fn (name, decl) =>
    1.26      if exists (fn space => Name_Space.declared space name) parents then I
    1.27      else
    1.28        (case export_decl thy name decl of
    1.29          NONE => I
    1.30 -      | SOME body => cons (name, XML.Elem (entity_markup space name, body))))
    1.31 +      | SOME body => cons (name, XML.Elem (entity_markup adjust_pos space name, body))))
    1.32    |> sort_by #1 |> map #2;
    1.33  
    1.34  
    1.35  (* present *)
    1.36  
    1.37 -fun present get_space get_decls export name thy =
    1.38 +fun present get_space get_decls export name adjust_pos thy =
    1.39    if Options.default_bool "export_theory" then
    1.40 -    (case export (map get_space (Theory.parents_of thy)) thy (get_space thy) (get_decls thy) of
    1.41 +    (case
    1.42 +      export (map get_space (Theory.parents_of thy)) thy adjust_pos (get_space thy) (get_decls thy)
    1.43 +     of
    1.44        [] => ()
    1.45      | body => Export.export thy ("theory/" ^ name) [YXML.string_of_body body])
    1.46    else ();
    1.47 @@ -42,7 +43,7 @@
    1.48  fun present_decls get_space get_decls =
    1.49    present get_space get_decls o export_decls;
    1.50  
    1.51 -fun setup_presentation f = Theory.setup (Thy_Info.add_presentation (K f));
    1.52 +val setup_presentation = Theory.setup o Thy_Info.add_presentation;
    1.53  
    1.54  
    1.55  (* types *)
    1.56 @@ -62,7 +63,7 @@
    1.57  
    1.58  in
    1.59  
    1.60 -val _ = setup_presentation (present_types (K (K export_type)) "types");
    1.61 +val _ = setup_presentation (present_types (K (K export_type)) "types" o #adjust_pos);
    1.62  
    1.63  end;
    1.64  
    1.65 @@ -87,7 +88,7 @@
    1.66  
    1.67  in
    1.68  
    1.69 -val _ = setup_presentation (present_consts export_const "consts");
    1.70 +val _ = setup_presentation (present_consts export_const "consts" o #adjust_pos);
    1.71  
    1.72  end;
    1.73