# HG changeset patch
# User wenzelm
# Date 1262201168 -3600
# Node ID b4efd0ef2f3eeb5c29c73514dbd4d90e28316fe7
# Parent  d3331251422047c73cac79cb6a0b56cc41c68d3b
tuned signature of isabelle.Position;

diff -r d33312514220 -r b4efd0ef2f3e src/Tools/jEdit/src/proofdocument/session.scala
--- a/src/Tools/jEdit/src/proofdocument/session.scala	Wed Dec 30 20:18:50 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/session.scala	Wed Dec 30 20:26:08 2009 +0100
@@ -106,7 +106,7 @@
       raw_results.event(result)
 
       val target: Option[Session.Entity] =
-        Position.id_of(result.props) match {
+        Position.get_id(result.props) match {
           case None => None
           case Some(id) => entities.get(id)
         }
diff -r d33312514220 -r b4efd0ef2f3e src/Tools/jEdit/src/proofdocument/state.scala
--- a/src/Tools/jEdit/src/proofdocument/state.scala	Wed Dec 30 20:18:50 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/state.scala	Wed Dec 30 20:26:08 2009 +0100
@@ -81,7 +81,7 @@
               case XML.Elem(Markup.FINISHED, _, _) => state.set_status(Command.Status.FINISHED)
               case XML.Elem(Markup.FAILED, _, _) => state.set_status(Command.Status.FAILED)
               case XML.Elem(kind, atts, body) =>
-                val (begin, end) = Position.offsets_of(atts)
+                val (begin, end) = Position.get_offsets(atts)
                 if (begin.isEmpty || end.isEmpty) state
                 else if (kind == Markup.ML_TYPING) {
                   val info = body.first.asInstanceOf[XML.Text].content   // FIXME proper match!?
@@ -94,10 +94,10 @@
                       state.add_markup(command.markup_node(
                         begin.get - 1, end.get - 1,
                         Command.RefInfo(
-                          Position.file_of(atts),
-                          Position.line_of(atts),
-                          Position.id_of(atts),
-                          Position.offset_of(atts))))
+                          Position.get_file(atts),
+                          Position.get_line(atts),
+                          Position.get_id(atts),
+                          Position.get_offset(atts))))
                     case _ => state
                   }
                 }