src/Pure/Syntax/syntax_phases.ML

 of parse/unparse operations.
 *)
 
 signature SYNTAX_PHASES =
 sig
+  val reports_of_scope: Position.T list -> Position.report list
   val decode_sort: term -> sort
   val decode_typ: term -> typ
   val decode_term: Proof.context ->
     Position.report_text list * term Exn.result -> Position.report_text list * term Exn.result
   val parse_ast_pattern: Proof.context -> string * string -> Ast.ast

      {case_class = markup_class ctxt,
       case_type = markup_type ctxt,
       case_const = markup_const ctxt,
       case_fixed = markup_free ctxt,
       case_default = K []});
+
+
+
+(** reports of implicit variable scope **)
+
+fun reports_of_scope [] = []
+  | reports_of_scope (def_pos :: ps) =
+      let
+        val id = serial ();
+        fun entity def = (Markup.entityN, Position.entity_properties_of def id def_pos);
+      in
+        map (rpair Markup.bound) (def_pos :: ps) @
+        ((def_pos, entity true) :: map (rpair (entity false)) ps)
+      end;
 
 
 
 (** decode parse trees **)