1.1 --- a/lib/jedit/plugin/isabelle/IsabelleDock.scala Sat Aug 23 23:07:28 2008 +0200
1.2 +++ b/lib/jedit/plugin/isabelle/IsabelleDock.scala Sat Aug 23 23:07:30 2008 +0200
1.3 @@ -61,7 +61,7 @@
1.4 val errorStyle = makeStyle("error", true, new Color(255, 160, 160))
1.5
1.6 IsabellePlugin.addPermanentConsumer (result =>
1.7 - if (result != null && !result.isSystem) {
1.8 + if (result != null && !result.is_system) {
1.9 SwingUtilities.invokeLater(new Runnable {
1.10 def run = {
1.11 val logic = IsabellePlugin.isabelle.session
1.12 @@ -70,13 +70,13 @@
1.13
1.14 val doc = pane.getDocument.asInstanceOf[StyledDocument]
1.15 val style = result.kind match {
1.16 - case IsabelleProcess.Result.Kind.WARNING => warningStyle
1.17 - case IsabelleProcess.Result.Kind.ERROR => errorStyle
1.18 - case IsabelleProcess.Result.Kind.TRACING => infoStyle
1.19 - case _ => if (result.isRaw) rawStyle else null
1.20 + case IsabelleProcess.Kind.WARNING => warningStyle
1.21 + case IsabelleProcess.Kind.ERROR => errorStyle
1.22 + case IsabelleProcess.Kind.TRACING => infoStyle
1.23 + case _ => if (result.is_raw) rawStyle else null
1.24 }
1.25 - doc.insertString(doc.getLength, result.result, style)
1.26 - if (!result.isRaw) doc.insertString(doc.getLength, "\n", style)
1.27 + doc.insertString(doc.getLength, IsabellePlugin.result_content(result), style)
1.28 + if (!result.is_raw) doc.insertString(doc.getLength, "\n", style)
1.29 pane.setCaretPosition(doc.getLength)
1.30 }
1.31 })
2.1 --- a/lib/jedit/plugin/isabelle/IsabellePlugin.scala Sat Aug 23 23:07:28 2008 +0200
2.2 +++ b/lib/jedit/plugin/isabelle/IsabellePlugin.scala Sat Aug 23 23:07:30 2008 +0200
2.3 @@ -7,18 +7,18 @@
2.4
2.5 package isabelle
2.6
2.7 -import isabelle.IsabelleProcess
2.8 -
2.9 import org.gjt.sp.jedit.EditPlugin
2.10 import org.gjt.sp.util.Log
2.11
2.12 import errorlist.DefaultErrorSource
2.13 import errorlist.ErrorSource
2.14
2.15 -import scala.collection.mutable.ListBuffer
2.16 import java.util.Properties
2.17 import java.lang.NumberFormatException
2.18
2.19 +import scala.collection.mutable.ListBuffer
2.20 +import scala.io.Source
2.21 +
2.22
2.23 /* Global state */
2.24
2.25 @@ -31,7 +31,7 @@
2.26
2.27 def idProperties(value: String) : Properties = {
2.28 val props = new Properties
2.29 - props.setProperty("id", value)
2.30 + props.setProperty(Markup.ID, value)
2.31 props
2.32 }
2.33
2.34 @@ -47,6 +47,11 @@
2.35 var isabelle: IsabelleProcess = null
2.36
2.37
2.38 + // result content
2.39 + def result_content(result: IsabelleProcess.Result) =
2.40 + XML.content(isabelle.result_tree(result)).mkString("")
2.41 +
2.42 +
2.43 // result consumers
2.44 type consumer = IsabelleProcess.Result => Boolean
2.45 private var consumers = new ListBuffer[consumer]
2.46 @@ -84,32 +89,37 @@
2.47
2.48 IsabellePlugin.addPermanentConsumer (result =>
2.49 if (result != null && result.props != null &&
2.50 - (result.kind == IsabelleProcess.Result.Kind.WARNING ||
2.51 - result.kind == IsabelleProcess.Result.Kind.ERROR)) {
2.52 + (result.kind == IsabelleProcess.Kind.WARNING ||
2.53 + result.kind == IsabelleProcess.Kind.ERROR)) {
2.54 val typ =
2.55 - if (result.kind == IsabelleProcess.Result.Kind.WARNING) ErrorSource.WARNING
2.56 + if (result.kind == IsabelleProcess.Kind.WARNING) ErrorSource.WARNING
2.57 else ErrorSource.ERROR
2.58 - val line = result.props.getProperty(IsabelleProcess.Property.LINE)
2.59 - val file = result.props.getProperty(IsabelleProcess.Property.FILE)
2.60 - if (line != null && file != null && result.result.length > 0) {
2.61 - val msg = result.result.split("\n")
2.62 - val err = new DefaultErrorSource.DefaultError(IsabellePlugin.errors,
2.63 - typ, file, Integer.parseInt(line) - 1, 0, 0, msg(0))
2.64 - for (i <- 1 to msg.length - 1)
2.65 - err.addExtraMessage(msg(i))
2.66 - IsabellePlugin.errors.addError(err)
2.67 + (Position.line_of(result.props), Position.file_of(result.props)) match {
2.68 + case (Some(line), Some(file)) =>
2.69 + val content = IsabellePlugin.result_content(result)
2.70 + if (content.length > 0) {
2.71 + val lines = Source.fromString(content).getLines
2.72 + val err = new DefaultErrorSource.DefaultError(IsabellePlugin.errors,
2.73 + typ, file, line - 1, 0, 0, lines.next)
2.74 + for (msg <- lines) err.addExtraMessage(msg)
2.75 + IsabellePlugin.errors.addError(err)
2.76 + }
2.77 + case _ =>
2.78 }
2.79 })
2.80
2.81 +
2.82 // Isabelle process
2.83 - IsabellePlugin.isabelle = new IsabelleProcess(Array("-m", "builtin_browser"), null)
2.84 + IsabellePlugin.isabelle =
2.85 + new IsabelleProcess("-mno_brackets", "-mno_type_brackets", "-mxsymbols")
2.86 thread = new Thread (new Runnable {
2.87 def run = {
2.88 var result: IsabelleProcess.Result = null
2.89 do {
2.90 try {
2.91 - result = IsabellePlugin.isabelle.results.take.asInstanceOf[IsabelleProcess.Result]
2.92 - } catch {
2.93 + result = IsabellePlugin.isabelle.results.take
2.94 + }
2.95 + catch {
2.96 case _: NullPointerException => result = null
2.97 case _: InterruptedException => result = null
2.98 }
2.99 @@ -117,7 +127,7 @@
2.100 System.err.println(result) // FIXME
2.101 IsabellePlugin.consume(result)
2.102 }
2.103 - if (result.kind == IsabelleProcess.Result.Kind.EXIT) {
2.104 + if (result.kind == IsabelleProcess.Kind.EXIT) {
2.105 result = null
2.106 IsabellePlugin.consume(null)
2.107 }
2.108 @@ -136,4 +146,3 @@
2.109 IsabellePlugin.errors = null
2.110 }
2.111 }
2.112 -