# HG changeset patch
# User wenzelm
# Date 1302534663 -7200
# Node ID 7c7cc7590eb38a1e27b86eda2037995b27c8d08c
# Parent  e2d22eb4aeb9f1da7c9bdf663b4f8504373f67ae
Name_Space.entry_markup: keep def position as separate properties;
uniform treatment of ML_def/ML_open/ML_struct as entities;
hyperlinks for all entities -- excluding ML_open/ML_struct for now;

diff -r e2d22eb4aeb9 -r 7c7cc7590eb3 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Sat Apr 09 23:29:50 2011 +0200
+++ b/src/Pure/General/markup.ML	Mon Apr 11 17:11:03 2011 +0200
@@ -71,10 +71,9 @@
   val ML_stringN: string val ML_string: T
   val ML_commentN: string val ML_comment: T
   val ML_malformedN: string val ML_malformed: T
-  val ML_defN: string val ML_def: T
-  val ML_openN: string val ML_open: T
-  val ML_structN: string val ML_struct: T
-  val ML_refN: string val ML_ref: T
+  val ML_defN: string
+  val ML_openN: string
+  val ML_structN: string
   val ML_typingN: string val ML_typing: T
   val ML_sourceN: string val ML_source: T
   val doc_sourceN: string val doc_source: T
@@ -264,10 +263,9 @@
 val (ML_commentN, ML_comment) = markup_elem "ML_comment";
 val (ML_malformedN, ML_malformed) = markup_elem "ML_malformed";
 
-val (ML_defN, ML_def) = markup_elem "ML_def";
-val (ML_openN, ML_open) = markup_elem "ML_open";
-val (ML_structN, ML_struct) = markup_elem "ML_struct";
-val (ML_refN, ML_ref) = markup_elem "ML_ref";
+val ML_defN = "ML_def";
+val ML_openN = "ML_open";
+val ML_structN = "ML_struct";
 val (ML_typingN, ML_typing) = markup_elem "ML_typing";
 
 
diff -r e2d22eb4aeb9 -r 7c7cc7590eb3 src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Sat Apr 09 23:29:50 2011 +0200
+++ b/src/Pure/General/markup.scala	Mon Apr 11 17:11:03 2011 +0200
@@ -120,6 +120,13 @@
   val FILE = "file"
   val ID = "id"
 
+  val DEF_LINE = "def_line"
+  val DEF_COLUMN = "def_column"
+  val DEF_OFFSET = "def_offset"
+  val DEF_END_OFFSET = "def_end_offset"
+  val DEF_FILE = "def_file"
+  val DEF_ID = "def_id"
+
   val POSITION_PROPERTIES = Set(LINE, COLUMN, OFFSET, END_OFFSET, FILE, ID)
 
   val POSITION = "position"
@@ -204,7 +211,6 @@
   val ML_DEF = "ML_def"
   val ML_OPEN = "ML_open"
   val ML_STRUCT = "ML_struct"
-  val ML_REF = "ML_ref"
   val ML_TYPING = "ML_typing"
 
 
diff -r e2d22eb4aeb9 -r 7c7cc7590eb3 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Sat Apr 09 23:29:50 2011 +0200
+++ b/src/Pure/General/name_space.ML	Mon Apr 11 17:11:03 2011 +0200
@@ -82,8 +82,9 @@
 
 fun entry_markup def kind (name, {pos, id, ...}: entry) =
   let
-    val occurrence = (if def then Markup.defN else Markup.refN, string_of_int id);
-    val props = occurrence :: Position.properties_of pos;
+    val props =
+      if def then (Markup.defN, string_of_int id) :: Position.properties_of pos
+      else (Markup.refN, string_of_int id) :: Position.def_properties_of pos;
   in Markup.properties props (Markup.entity kind name) end;
 
 fun print_entry def kind (name, entry) =
diff -r e2d22eb4aeb9 -r 7c7cc7590eb3 src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Sat Apr 09 23:29:50 2011 +0200
+++ b/src/Pure/General/position.ML	Mon Apr 11 17:11:03 2011 +0200
@@ -28,6 +28,7 @@
   val put_id: string -> T -> T
   val of_properties: Properties.T -> T
   val properties_of: T -> Properties.T
+  val def_properties_of: T -> Properties.T
   val default_properties: T -> Properties.T -> Properties.T
   val markup: T -> Markup.T -> Markup.T
   val is_reported: T -> bool
@@ -142,6 +143,8 @@
   value Markup.lineN i @ value Markup.columnN j @
   value Markup.offsetN k @ value Markup.end_offsetN l @ props;
 
+val def_properties_of = properties_of #> (map (fn (x, y) => ("def_" ^ x, y)));
+
 fun default_properties default props =
   if exists (member (op =) Markup.position_properties o #1) props then props
   else properties_of default @ props;
diff -r e2d22eb4aeb9 -r 7c7cc7590eb3 src/Pure/General/position.scala
--- a/src/Pure/General/position.scala	Sat Apr 09 23:29:50 2011 +0200
+++ b/src/Pure/General/position.scala	Mon Apr 11 17:11:03 2011 +0200
@@ -37,5 +37,15 @@
       }
   }
 
-  def purge(props: T): T = props.filterNot(p => Markup.POSITION_PROPERTIES(p._1))
+  private val purge_pos = Map(
+    Markup.DEF_LINE -> Markup.LINE,
+    Markup.DEF_COLUMN -> Markup.COLUMN,
+    Markup.DEF_OFFSET -> Markup.OFFSET,
+    Markup.DEF_END_OFFSET -> Markup.END_OFFSET,
+    Markup.DEF_FILE -> Markup.FILE,
+    Markup.DEF_ID -> Markup.ID)
+
+  def purge(props: T): T =
+    for ((x, y) <- props if !Markup.POSITION_PROPERTIES(x))
+      yield (if (purge_pos.isDefinedAt(x)) (purge_pos(x), y) else (x, y))
 }
diff -r e2d22eb4aeb9 -r 7c7cc7590eb3 src/Pure/ML/ml_compiler_polyml-5.3.ML
--- a/src/Pure/ML/ml_compiler_polyml-5.3.ML	Sat Apr 09 23:29:50 2011 +0200
+++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML	Mon Apr 11 17:11:03 2011 +0200
@@ -40,19 +40,21 @@
         SOME (Context.Proof ctxt) => Context_Position.report_text ctxt
       | _ => Position.report_text);
 
-    fun report_decl markup loc decl =
-      report_text (position_of loc) Markup.ML_ref
-        (Markup.markup (Position.markup (position_of decl) markup) "");
+    fun report_entity kind loc decl =
+      report_text (position_of loc)
+        (Markup.entityN, (Markup.kindN, kind) :: Position.def_properties_of (position_of decl)) "";
 
     fun report loc (PolyML.PTtype types) =
           cons (fn () =>
             PolyML.NameSpace.displayTypeExpression (types, depth, space)
             |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
             |> report_text (position_of loc) Markup.ML_typing)
-      | report loc (PolyML.PTdeclaredAt decl) = cons (fn () => report_decl Markup.ML_def loc decl)
-      | report loc (PolyML.PTopenedAt decl) = cons (fn () => report_decl Markup.ML_open loc decl)
+      | report loc (PolyML.PTdeclaredAt decl) =
+          cons (fn () => report_entity Markup.ML_defN loc decl)
+      | report loc (PolyML.PTopenedAt decl) =
+          cons (fn () => report_entity Markup.ML_openN loc decl)
       | report loc (PolyML.PTstructureAt decl) =
-          cons (fn () => report_decl Markup.ML_struct loc decl)
+          cons (fn () => report_entity Markup.ML_structN loc decl)
       | report _ (PolyML.PTnextSibling tree) = report_tree (tree ())
       | report _ (PolyML.PTfirstChild tree) = report_tree (tree ())
       | report _ _ = I
diff -r e2d22eb4aeb9 -r 7c7cc7590eb3 src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Sat Apr 09 23:29:50 2011 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Mon Apr 11 17:11:03 2011 +0200
@@ -16,23 +16,23 @@
 import org.gjt.sp.jedit.{View, jEdit, Buffer, TextUtilities}
 
 
-private class Internal_Hyperlink(start: Int, end: Int, line: Int, ref_offset: Int)
+private class Internal_Hyperlink(start: Int, end: Int, line: Int, def_offset: Int)
   extends AbstractHyperlink(start, end, line, "")
 {
   override def click(view: View) {
-    view.getTextArea.moveCaretPosition(ref_offset)
+    view.getTextArea.moveCaretPosition(def_offset)
   }
 }
 
-class External_Hyperlink(start: Int, end: Int, line: Int, ref_file: String, ref_line: Int)
+class External_Hyperlink(start: Int, end: Int, line: Int, def_file: String, def_line: Int)
   extends AbstractHyperlink(start, end, line, "")
 {
   override def click(view: View) = {
-    Isabelle.system.source_file(ref_file) match {
+    Isabelle.system.source_file(def_file) match {
       case None =>
-        Library.error_dialog(view, "File not found", "Could not find source file " + ref_file)
+        Library.error_dialog(view, "File not found", "Could not find source file " + def_file)
       case Some(file) =>
-        jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + ref_line))
+        jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + def_line))
     }
   }
 }
@@ -49,22 +49,26 @@
           val markup =
             snapshot.select_markup(Text.Range(buffer_offset, buffer_offset + 1)) {
               // FIXME Isar_Document.Hyperlink extractor
-              case Text.Info(info_range, XML.Elem(Markup(Markup.ML_REF, _),
-                  List(XML.Elem(Markup(Markup.ML_DEF, props), _)))) =>
+              case Text.Info(info_range,
+                  XML.Elem(Markup(Markup.ENTITY, props), _))
+                if (props.find(
+                  { case (Markup.KIND, Markup.ML_OPEN) => true
+                    case (Markup.KIND, Markup.ML_STRUCT) => true
+                    case _ => false }).isEmpty) =>
                 val Text.Range(begin, end) = info_range
                 val line = buffer.getLineOfOffset(begin)
                 (Position.File.unapply(props), Position.Line.unapply(props)) match {
-                  case (Some(ref_file), Some(ref_line)) =>
-                    new External_Hyperlink(begin, end, line, ref_file, ref_line)
+                  case (Some(def_file), Some(def_line)) =>
+                    new External_Hyperlink(begin, end, line, def_file, def_line)
                   case _ =>
                     (props, props) match {
-                      case (Position.Id(ref_id), Position.Offset(ref_offset)) =>
-                        snapshot.lookup_command(ref_id) match {
-                          case Some(ref_cmd) =>
-                            snapshot.node.command_start(ref_cmd) match {
-                              case Some(ref_cmd_start) =>
+                      case (Position.Id(def_id), Position.Offset(def_offset)) =>
+                        snapshot.lookup_command(def_id) match {
+                          case Some(def_cmd) =>
+                            snapshot.node.command_start(def_cmd) match {
+                              case Some(def_cmd_start) =>
                                 new Internal_Hyperlink(begin, end, line,
-                                  snapshot.convert(ref_cmd_start + ref_cmd.decode(ref_offset)))
+                                  snapshot.convert(def_cmd_start + def_cmd.decode(def_offset)))
                               case None => null
                             }
                           case None => null