--- 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)
}
}
--- 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")
--- 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 {
--- 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 */