# HG changeset patch
# User wenzelm
# Date 1417534811 -3600
# Node ID 12a689755c3d9b99079b26e111337abbe7a12d96
# Parent  cf255dc2b48fe281e41ca93f5e79dfaeb9f7b6e0
tuned signature -- more explicit types;

diff -r cf255dc2b48f -r 12a689755c3d src/Pure/General/untyped.scala
--- a/src/Pure/General/untyped.scala	Tue Dec 02 16:10:11 2014 +0100
+++ b/src/Pure/General/untyped.scala	Tue Dec 02 16:40:11 2014 +0100
@@ -20,8 +20,8 @@
     }
   }
 
-  def get(obj: AnyRef, x: String): AnyRef =
-    if (obj == null) null
+  def get[A](obj: AnyRef, x: String): A =
+    if (obj == null) null.asInstanceOf[A]
     else {
       val iterator =
         for {
@@ -32,7 +32,7 @@
           field.setAccessible(true)
           field.get(obj)
         }
-      if (iterator.hasNext) iterator.next
+      if (iterator.hasNext) iterator.next.asInstanceOf[A]
       else error("No field " + quote(x) + " for " + obj)
     }
 }
diff -r cf255dc2b48f -r 12a689755c3d src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Tue Dec 02 16:10:11 2014 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Tue Dec 02 16:40:11 2014 +0100
@@ -288,7 +288,7 @@
 
   def syntax_changed()
   {
-    Untyped.get(buffer, "lineMgr").asInstanceOf[LineManager].setFirstInvalidLineContext(0)
+    Untyped.get[LineManager](buffer, "lineMgr").setFirstInvalidLineContext(0)
     for (text_area <- JEdit_Lib.jedit_text_areas(buffer)) {
       val c = Class.forName("org.gjt.sp.jedit.textarea.TextArea")
       val m = c.getDeclaredMethod("foldStructureChanged")
diff -r cf255dc2b48f -r 12a689755c3d src/Tools/jEdit/src/pide_docking_framework.scala
--- a/src/Tools/jEdit/src/pide_docking_framework.scala	Tue Dec 02 16:10:11 2014 +0100
+++ b/src/Tools/jEdit/src/pide_docking_framework.scala	Tue Dec 02 16:40:11 2014 +0100
@@ -36,21 +36,18 @@
       val detach_operation: Option[() => Unit] =
         container match {
           case floating: FloatingWindowContainer =>
-            val entry = Untyped.get(floating, "entry")
-            val win = Untyped.get(entry, "win")
-            win match {
+            Untyped.get[AnyRef](Untyped.get[AnyRef](floating, "entry"), "win") match {
               case dockable: Dockable => dockable.detach_operation
               case _ => None
             }
 
           case panel: PanelWindowContainer =>
-            val entries =
-              Untyped.get(panel, "dockables").asInstanceOf[java.util.List[AnyRef]].toArray
+            val entries = Untyped.get[java.util.List[AnyRef]](panel, "dockables").toArray
             val wins =
               (for {
                 entry <- entries.iterator
-                if Untyped.get(Untyped.get(entry, "factory"), "name") == dockable_name
-                win = Untyped.get(entry, "win")
+                if Untyped.get[String](Untyped.get(entry, "factory"), "name") == dockable_name
+                win = Untyped.get[Any](entry, "win")
                 if win != null
               } yield win).toList
             wins match {
diff -r cf255dc2b48f -r 12a689755c3d src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Tue Dec 02 16:10:11 2014 +0100
+++ b/src/Tools/jEdit/src/token_markup.scala	Tue Dec 02 16:40:11 2014 +0100
@@ -193,19 +193,18 @@
   }
 
   def buffer_line_context(buffer: JEditBuffer, line: Int): Line_Context =
-    Untyped.get(buffer, "lineMgr") match {
-      case line_mgr: LineManager =>
-        def context =
-          line_mgr.getLineContext(line) match {
-            case c: Line_Context => Some(c)
-            case _ => None
-          }
-        context getOrElse {
-          buffer.markTokens(line, DummyTokenHandler.INSTANCE)
-          context getOrElse Line_Context.init
-        }
-      case _ => Line_Context.init
+  {
+    val line_mgr = Untyped.get[LineManager](buffer, "lineMgr")
+    def context =
+      line_mgr.getLineContext(line) match {
+        case c: Line_Context => Some(c)
+        case _ => None
+      }
+    context getOrElse {
+      buffer.markTokens(line, DummyTokenHandler.INSTANCE)
+      context getOrElse Line_Context.init
     }
+  }
 
 
   /* line tokens */