# HG changeset patch
# User wenzelm
# Date 1575643989 -3600
# Node ID 877316c54ed3c12964996f00ebb343cc6f93973d
# Parent  adf5e53d2b2b7d6c5848a80078b6722f36dee4ab
clarified signature;

diff -r adf5e53d2b2b -r 877316c54ed3 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Dec 06 15:44:55 2019 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Dec 06 15:53:09 2019 +0100
@@ -1240,7 +1240,7 @@
 
 (* theory export *)
 
-val _ = Export_Theory.setup_presentation (fn {adjust_pos, ...} => fn thy =>
+val _ = Export_Theory.setup_presentation (fn context => fn thy =>
   let
     val parents = map (Data.get o Context.Theory) (Theory.parents_of thy);
     val datatypes =
@@ -1249,8 +1249,7 @@
           if exists (fn tab => Symtab.defined tab name) parents then I
           else
             let
-              val pos_properties =
-                Position.offset_properties_of (adjust_pos pos) @ Position.id_properties_of pos;
+              val pos_properties = Thy_Info.adjust_pos_properties context pos;
               val typ = Logic.unvarifyT_global T;
               val constrs = map Logic.unvarify_global ctrs;
               val typargs = rev (fold Term.add_tfrees (Logic.mk_type typ :: constrs) []);
diff -r adf5e53d2b2b -r 877316c54ed3 src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Fri Dec 06 15:44:55 2019 +0100
+++ b/src/Pure/Thy/export_theory.ML	Fri Dec 06 15:53:09 2019 +0100
@@ -121,19 +121,18 @@
 
 (* presentation *)
 
-val _ = setup_presentation (fn {adjust_pos, ...} => fn thy =>
+val _ = setup_presentation (fn context => fn thy =>
   let
     val parents = Theory.parents_of thy;
     val rep_tsig = Type.rep_tsig (Sign.tsig_of thy);
 
     val thy_ctxt = Proof_Context.init_global thy;
 
+    val pos_properties = Thy_Info.adjust_pos_properties context;
+
 
     (* spec rules *)
 
-    fun position_properties pos =
-      Position.offset_properties_of (adjust_pos pos) @ Position.id_properties_of pos;
-
     fun spec_rule_content {pos, name, rough_classification, terms, rules} =
       let
         val spec =
@@ -141,7 +140,7 @@
           |> Term_Subst.zero_var_indexes_list
           |> map Logic.unvarify_global;
       in
-       {props = position_properties pos,
+       {props = pos_properties pos,
         name = name,
         rough_classification = rough_classification,
         typargs = rev (fold Term.add_tfrees spec []),
@@ -154,7 +153,7 @@
     (* entities *)
 
     fun make_entity_markup name xname pos serial =
-      let val props = position_properties pos @ Markup.serial_properties serial;
+      let val props = pos_properties pos @ Markup.serial_properties serial;
       in (Markup.entityN, (Markup.nameN, name) :: (Markup.xnameN, xname) :: props) end;
 
     fun entity_markup space name =
diff -r adf5e53d2b2b -r 877316c54ed3 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Fri Dec 06 15:44:55 2019 +0100
+++ b/src/Pure/Thy/thy_info.ML	Fri Dec 06 15:53:09 2019 +0100
@@ -10,6 +10,7 @@
   type presentation_context =
     {options: Options.T, file_pos: Position.T, adjust_pos: Position.T -> Position.T,
       segments: Thy_Output.segment list}
+  val adjust_pos_properties: presentation_context -> Position.T -> Properties.T
   val apply_presentation: presentation_context -> theory -> unit
   val add_presentation: (presentation_context -> theory -> unit) -> theory -> theory
   val get_names: unit -> string list
@@ -38,6 +39,9 @@
   {options: Options.T, file_pos: Position.T, adjust_pos: Position.T -> Position.T,
     segments: Thy_Output.segment list};
 
+fun adjust_pos_properties (context: presentation_context) pos =
+  Position.offset_properties_of (#adjust_pos context pos) @ Position.id_properties_of pos;
+
 structure Presentation = Theory_Data
 (
   type T = ((presentation_context -> theory -> unit) * stamp) list;