--- a/.hgignore Mon Jan 11 16:45:02 2010 +0100
+++ b/.hgignore Mon Jan 11 23:11:31 2010 +0100
@@ -24,4 +24,7 @@
^doc-src/.*\.rao
^doc-src/.*\.toc
-
+^src/Tools/jEdit/nbproject/private/
+^src/Tools/jEdit/build/
+^src/Tools/jEdit/dist/
+^src/Tools/jEdit/contrib/
--- a/src/Pure/General/exn.scala Mon Jan 11 16:45:02 2010 +0100
+++ b/src/Pure/General/exn.scala Mon Jan 11 23:11:31 2010 +0100
@@ -1,7 +1,7 @@
/* Title: Pure/General/exn.scala
Author: Makarius
-Extra support for exceptions.
+Extra support for exceptions (arbitrary throwables).
*/
package isabelle
@@ -13,11 +13,11 @@
sealed abstract class Result[A]
case class Res[A](val result: A) extends Result[A]
- case class Exn[A](val exn: Exception) extends Result[A]
+ case class Exn[A](val exn: Throwable) extends Result[A]
def capture[A](e: => A): Result[A] =
try { Res(e) }
- catch { case exn: RuntimeException => Exn[A](exn) } // FIXME *all* exceptions (!?), cf. ML version
+ catch { case exn: Throwable => Exn[A](exn) }
def release[A](result: Result[A]): A =
result match {
--- a/src/Pure/General/scan.scala Mon Jan 11 16:45:02 2010 +0100
+++ b/src/Pure/General/scan.scala Mon Jan 11 23:11:31 2010 +0100
@@ -179,7 +179,7 @@
private def quoted(quote: String): Parser[String] =
{
quote ~
- rep(many1(sym => sym != quote && sym != "\\" && Symbol.is_closed(sym)) |
+ rep(many1(sym => sym != quote && sym != "\\" && Symbol.is_wellformed(sym)) |
"\\" + quote | "\\\\" |
(("""\\\d\d\d""".r) ^? { case x if x.substring(1, 4).toInt <= 255 => x })) ~
quote ^^ { case x ~ ys ~ z => x + ys.mkString + z }
@@ -191,7 +191,7 @@
val body = source.substring(1, source.length - 1)
if (body.exists(_ == '\\')) {
val content =
- rep(many1(sym => sym != quote && sym != "\\" && Symbol.is_closed(sym)) |
+ rep(many1(sym => sym != quote && sym != "\\" && Symbol.is_wellformed(sym)) |
"\\" ~> (quote | "\\" | """\d\d\d""".r ^^ { case x => x.toInt.toChar.toString }))
parseAll(content ^^ (_.mkString), body).get
}
@@ -203,7 +203,7 @@
private def verbatim: Parser[String] =
{
- "{*" ~ rep(many1(sym => sym != "*" && Symbol.is_closed(sym)) | """\*(?!\})""".r) ~ "*}" ^^
+ "{*" ~ rep(many1(sym => sym != "*" && Symbol.is_wellformed(sym)) | """\*(?!\})""".r) ~ "*}" ^^
{ case x ~ ys ~ z => x + ys.mkString + z }
}.named("verbatim")
@@ -219,7 +219,7 @@
def comment: Parser[String] = new Parser[String]
{
val comment_text =
- rep(many1(sym => sym != "*" && sym != "(" && Symbol.is_closed(sym)) |
+ rep(many1(sym => sym != "*" && sym != "(" && Symbol.is_wellformed(sym)) |
"""\*(?!\))|\((?!\*)""".r)
val comment_open = "(*" ~ comment_text ^^^ ()
val comment_close = comment_text ~ "*)" ^^^ ()
@@ -276,7 +276,7 @@
val sym_ident =
(many1(symbols.is_symbolic_char) |
- one(sym => symbols.is_symbolic(sym) & Symbol.is_closed(sym))) ^^
+ one(sym => symbols.is_symbolic(sym) & Symbol.is_wellformed(sym))) ^^
(x => Token(Token_Kind.SYM_IDENT, x))
val space = many1(symbols.is_blank) ^^ (x => Token(Token_Kind.SPACE, x))
--- a/src/Pure/General/symbol.scala Mon Jan 11 16:45:02 2010 +0100
+++ b/src/Pure/General/symbol.scala Mon Jan 11 23:11:31 2010 +0100
@@ -23,6 +23,8 @@
\^? [A-Za-z][A-Za-z0-9_']* |
\^raw: [\x20-\x7e\u0100-\uffff && [^.>]]* ) >""")
+ // FIXME cover bad surrogates!?
+ // FIXME check wrt. ML version
private val bad_symbol = new Regex("(?xs) (?!" + symbol + ")" +
""" \\ < (?: (?! \s | [\"`\\] | \(\* | \*\) | \{\* | \*\} ) . )*""")
@@ -32,14 +34,10 @@
/* basic matching */
- def is_closed(c: Char): Boolean =
- !(c == '\\' || Character.isHighSurrogate(c))
+ def is_plain(c: Char): Boolean = !(c == '\\' || '\ud800' <= c && c <= '\udfff')
- def is_closed(s: CharSequence): Boolean =
- {
- if (s.length == 1) is_closed(s.charAt(0))
- else !bad_symbol.pattern.matcher(s).matches
- }
+ def is_wellformed(s: CharSequence): Boolean =
+ s.length == 1 && is_plain(s.charAt(0)) || !bad_symbol.pattern.matcher(s).matches
class Matcher(text: CharSequence)
{
@@ -47,7 +45,7 @@
def apply(start: Int, end: Int): Int =
{
require(0 <= start && start < end && end <= text.length)
- if (is_closed(text.charAt(start))) 1
+ if (is_plain(text.charAt(start))) 1
else {
matcher.region(start, end).lookingAt
matcher.group.length
@@ -177,7 +175,7 @@
}
}
decl.split("\\s+").toList match {
- case sym :: props if sym.length > 1 && is_closed(sym) => (sym, read_props(props))
+ case sym :: props if sym.length > 1 && is_wellformed(sym) => (sym, read_props(props))
case _ => err()
}
}
--- a/src/Pure/General/xml.scala Mon Jan 11 16:45:02 2010 +0100
+++ b/src/Pure/General/xml.scala Mon Jan 11 23:11:31 2010 +0100
@@ -10,8 +10,6 @@
import java.lang.ref.WeakReference
import javax.xml.parsers.DocumentBuilderFactory
-import org.w3c.dom.{Node, Document}
-
object XML
{
@@ -151,15 +149,15 @@
/* document object model (W3C DOM) */
- def get_data(node: Node): Option[XML.Tree] =
+ def get_data(node: org.w3c.dom.Node): Option[XML.Tree] =
node.getUserData(Markup.DATA) match {
case tree: XML.Tree => Some(tree)
case _ => None
}
- def document_node(doc: Document, tree: Tree): Node =
+ def document_node(doc: org.w3c.dom.Document, tree: Tree): org.w3c.dom.Node =
{
- def DOM(tr: Tree): Node = tr match {
+ def DOM(tr: Tree): org.w3c.dom.Node = tr match {
case Elem(Markup.DATA, Nil, List(data, t)) =>
val node = DOM(t)
node.setUserData(Markup.DATA, data, null)
--- a/src/Pure/Isar/outer_lex.scala Mon Jan 11 16:45:02 2010 +0100
+++ b/src/Pure/Isar/outer_lex.scala Mon Jan 11 23:11:31 2010 +0100
@@ -48,7 +48,7 @@
def is_text: Boolean = is_xname || kind == Token_Kind.VERBATIM
def is_space: Boolean = kind == Token_Kind.SPACE
def is_comment: Boolean = kind == Token_Kind.COMMENT
- def is_proper: Boolean = !(is_space || is_comment)
+ def is_ignored: Boolean = is_space || is_comment
def is_unparsed: Boolean = kind == Token_Kind.UNPARSED
def content: String =
--- a/src/Pure/Isar/outer_parse.scala Mon Jan 11 16:45:02 2010 +0100
+++ b/src/Pure/Isar/outer_parse.scala Mon Jan 11 23:11:31 2010 +0100
@@ -20,7 +20,7 @@
def filter_proper = true
private def proper(in: Input): Input =
- if (in.atEnd || in.first.is_proper || !filter_proper) in
+ if (in.atEnd || !in.first.is_ignored || !filter_proper) in
else proper(in.rest)
def token(s: String, pred: Elem => Boolean): Parser[Elem] = new Parser[Elem]
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/session.scala Mon Jan 11 23:11:31 2010 +0100
@@ -0,0 +1,250 @@
+/*
+ * Isabelle session, potentially with running prover
+ *
+ * @author Makarius
+ */
+
+package isabelle
+
+
+import scala.actors.TIMEOUT
+import scala.actors.Actor._
+
+
+object Session
+{
+ /* events */
+
+ case object Global_Settings
+
+
+ /* managed entities */
+
+ type Entity_ID = String
+
+ trait Entity
+ {
+ val id: Entity_ID
+ def consume(session: Session, message: XML.Tree): Unit
+ }
+}
+
+
+class Session(system: Isabelle_System)
+{
+ /* pervasive event buses */
+
+ val global_settings = new Event_Bus[Session.Global_Settings.type]
+ val raw_results = new Event_Bus[Isabelle_Process.Result]
+ val results = new Event_Bus[Command]
+
+ val command_change = new Event_Bus[Command]
+
+
+ /* unique ids */
+
+ private var id_count: BigInt = 0
+ def create_id(): Session.Entity_ID = synchronized { id_count += 1; "j" + id_count }
+
+
+
+ /** main actor **/
+
+ @volatile private var syntax = new Outer_Syntax(system.symbols)
+ def current_syntax: Outer_Syntax = syntax
+
+ @volatile private var entities = Map[Session.Entity_ID, Session.Entity]()
+ def lookup_entity(id: Session.Entity_ID): Option[Session.Entity] = entities.get(id)
+ def lookup_command(id: Session.Entity_ID): Option[Command] =
+ lookup_entity(id) match {
+ case Some(cmd: Command) => Some(cmd)
+ case _ => None
+ }
+
+ private case class Start(timeout: Int, args: List[String])
+ private case object Stop
+ private case class Begin_Document(path: String)
+
+ private val session_actor = actor {
+
+ var prover: Isabelle_Process with Isar_Document = null
+
+ def register(entity: Session.Entity) { entities += (entity.id -> entity) }
+
+ var documents = Map[Isar_Document.Document_ID, Document]()
+ def register_document(doc: Document) { documents += (doc.id -> doc) }
+
+
+ /* document changes */
+
+ def handle_change(change: Change)
+ {
+ require(change.parent.isDefined)
+
+ val (changes, doc) = change.result.join
+ val id_changes = changes map {
+ case (c1, c2) =>
+ (c1.map(_.id).getOrElse(""),
+ c2 match {
+ case None => None
+ case Some(command) =>
+ if (!lookup_command(command.id).isDefined) {
+ register(command)
+ prover.define_command(command.id, system.symbols.encode(command.source))
+ }
+ Some(command.id)
+ })
+ }
+ register_document(doc)
+ prover.edit_document(change.parent.get.id, doc.id, id_changes)
+ }
+
+
+ /* prover results */
+
+ def bad_result(result: Isabelle_Process.Result)
+ {
+ System.err.println("Ignoring prover result: " + result)
+ }
+
+ def handle_result(result: Isabelle_Process.Result)
+ {
+ raw_results.event(result)
+
+ val target_id: Option[Session.Entity_ID] = Position.get_id(result.props)
+ val target: Option[Session.Entity] =
+ target_id match {
+ case None => None
+ case Some(id) => lookup_entity(id)
+ }
+ if (target.isDefined) target.get.consume(this, result.message)
+ else if (result.kind == Isabelle_Process.Kind.STATUS) {
+ // global status message
+ result.body match {
+
+ // document state assigment
+ case List(XML.Elem(Markup.ASSIGN, _, edits)) if target_id.isDefined =>
+ documents.get(target_id.get) match {
+ case Some(doc) =>
+ val states =
+ for {
+ XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _)
+ <- edits
+ cmd <- lookup_command(cmd_id)
+ } yield {
+ val st = cmd.assign_state(state_id)
+ register(st)
+ (cmd, st)
+ }
+ doc.assign_states(states)
+ case None => bad_result(result)
+ }
+
+ // command and keyword declarations
+ case List(XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _)) =>
+ syntax += (name, kind)
+ case List(XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _)) =>
+ syntax += name
+
+ case _ => if (!result.is_ready) bad_result(result)
+ }
+ }
+ else if (result.kind == Isabelle_Process.Kind.EXIT)
+ prover = null
+ else if (result.kind != Isabelle_Process.Kind.STDIN && !result.is_raw)
+ bad_result(result)
+ }
+
+
+ /* prover startup */
+
+ def startup_error(): String =
+ {
+ val buf = new StringBuilder
+ while (
+ receiveWithin(0) {
+ case result: Isabelle_Process.Result =>
+ if (result.is_raw) {
+ for (text <- XML.content(result.message))
+ buf.append(text)
+ }
+ true
+ case TIMEOUT => false
+ }) {}
+ buf.toString
+ }
+
+ def prover_startup(timeout: Int): Option[String] =
+ {
+ receiveWithin(timeout) {
+ case result: Isabelle_Process.Result
+ if result.kind == Isabelle_Process.Kind.INIT =>
+ while (receive {
+ case result: Isabelle_Process.Result =>
+ handle_result(result); !result.is_ready
+ }) {}
+ None
+
+ case result: Isabelle_Process.Result
+ if result.kind == Isabelle_Process.Kind.EXIT =>
+ Some(startup_error())
+
+ case TIMEOUT => // FIXME clarify
+ prover.kill; Some(startup_error())
+ }
+ }
+
+
+ /* main loop */
+
+ val xml_cache = new XML.Cache(131071)
+
+ loop {
+ react {
+ case Start(timeout, args) =>
+ if (prover == null) {
+ prover = new Isabelle_Process(system, self, args:_*) with Isar_Document
+ val origin = sender
+ val opt_err = prover_startup(timeout)
+ if (opt_err.isDefined) prover = null
+ origin ! opt_err
+ }
+ else reply(None)
+
+ case Stop => // FIXME clarify; synchronous
+ if (prover != null) {
+ prover.kill
+ prover = null
+ }
+
+ case Begin_Document(path: String) if prover != null =>
+ val id = create_id()
+ val doc = Document.empty(id)
+ register_document(doc)
+ prover.begin_document(id, path)
+ reply(doc)
+
+ case change: Change if prover != null =>
+ handle_change(change)
+
+ case result: Isabelle_Process.Result =>
+ handle_result(result.cache(xml_cache))
+
+ case bad if prover != null =>
+ System.err.println("session_actor: ignoring bad message " + bad)
+ }
+ }
+ }
+
+
+ /* main methods */
+
+ def start(timeout: Int, args: List[String]): Option[String] =
+ (session_actor !? Start(timeout, args)).asInstanceOf[Option[String]]
+
+ def stop() { session_actor ! Stop }
+ def input(change: Change) { session_actor ! change }
+
+ def begin_document(path: String): Document =
+ (session_actor !? Begin_Document(path)).asInstanceOf[Document]
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/change.scala Mon Jan 11 23:11:31 2010 +0100
@@ -0,0 +1,42 @@
+/*
+ * Changes of plain text
+ *
+ * @author Fabian Immler, TU Munich
+ * @author Makarius
+ */
+
+package isabelle
+
+
+class Change(
+ val id: Isar_Document.Document_ID,
+ val parent: Option[Change],
+ val edits: List[Text_Edit],
+ val result: Future[(List[Document.Edit], Document)])
+{
+ def ancestors: Iterator[Change] = new Iterator[Change]
+ {
+ private var state: Option[Change] = Some(Change.this)
+ def hasNext = state.isDefined
+ def next =
+ state match {
+ case Some(change) => state = change.parent; change
+ case None => throw new NoSuchElementException("next on empty iterator")
+ }
+ }
+
+ def join_document: Document = result.join._2
+ def is_assigned: Boolean = result.is_finished && join_document.assignment.is_finished
+
+ def edit(session: Session, edits: List[Text_Edit]): Change =
+ {
+ val new_id = session.create_id()
+ val result: Future[(List[Document.Edit], Document)] =
+ Future.fork {
+ val old_doc = join_document
+ old_doc.await_assignment
+ Document.text_edits(session, old_doc, new_id, edits)
+ }
+ new Change(new_id, Some(this), edits, result)
+ }
+}
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/command.scala Mon Jan 11 23:11:31 2010 +0100
@@ -0,0 +1,100 @@
+/*
+ * Prover commands with semantic state
+ *
+ * @author Johannes Hölzl, TU Munich
+ * @author Fabian Immler, TU Munich
+ */
+
+package isabelle
+
+
+import scala.actors.Actor, Actor._
+import scala.collection.mutable
+
+
+object Command
+{
+ object Status extends Enumeration
+ {
+ val UNPROCESSED = Value("UNPROCESSED")
+ val FINISHED = Value("FINISHED")
+ val FAILED = Value("FAILED")
+ }
+
+ case class HighlightInfo(highlight: String) { override def toString = highlight }
+ case class TypeInfo(ty: String)
+ case class RefInfo(file: Option[String], line: Option[Int],
+ command_id: Option[String], offset: Option[Int])
+}
+
+
+class Command(
+ val id: Isar_Document.Command_ID,
+ val span: Thy_Syntax.Span)
+ extends Session.Entity
+{
+ /* classification */
+
+ def is_command: Boolean = !span.isEmpty && span.first.is_command
+ def is_ignored: Boolean = span.forall(_.is_ignored)
+ def is_malformed: Boolean = !is_command && !is_ignored
+
+ def name: String = if (is_command) span.first.content else ""
+ override def toString = if (is_command) name else if (is_ignored) "<ignored>" else "<malformed>"
+
+
+ /* source text */
+
+ val source: String = span.map(_.source).mkString
+ def source(i: Int, j: Int): String = source.substring(i, j)
+ def length: Int = source.length
+
+ lazy val symbol_index = new Symbol.Index(source)
+
+
+ /* accumulated messages */
+
+ @volatile protected var state = new State(this)
+ def current_state: State = state
+
+ private case class Consume(session: Session, message: XML.Tree)
+ private case object Assign
+
+ private val accumulator = actor {
+ var assigned = false
+ loop {
+ react {
+ case Consume(session: Session, message: XML.Tree) if !assigned =>
+ state = state.+(session, message)
+
+ case Assign =>
+ assigned = true // single assignment
+ reply(())
+
+ case bad => System.err.println("command accumulator: ignoring bad message " + bad)
+ }
+ }
+ }
+
+ def consume(session: Session, message: XML.Tree) { accumulator ! Consume(session, message) }
+
+ def assign_state(state_id: Isar_Document.State_ID): Command =
+ {
+ val cmd = new Command(state_id, span)
+ accumulator !? Assign
+ cmd.state = current_state
+ cmd
+ }
+
+
+ /* markup */
+
+ lazy val empty_markup = new Markup_Text(Nil, source)
+
+ def markup_node(begin: Int, end: Int, info: Any): Markup_Tree =
+ {
+ val start = symbol_index.decode(begin)
+ val stop = symbol_index.decode(end)
+ new Markup_Tree(new Markup_Node(start, stop, info), Nil)
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/document.scala Mon Jan 11 23:11:31 2010 +0100
@@ -0,0 +1,197 @@
+/*
+ * Document as editable list of commands
+ *
+ * @author Makarius
+ */
+
+package isabelle
+
+
+object Document
+{
+ /* command start positions */
+
+ def command_starts(commands: Linear_Set[Command]): Iterator[(Command, Int)] =
+ {
+ var offset = 0
+ for (cmd <- commands.elements) yield {
+ val start = offset
+ offset += cmd.length
+ (cmd, start)
+ }
+ }
+
+
+ /* empty document */
+
+ def empty(id: Isar_Document.Document_ID): Document =
+ {
+ val doc = new Document(id, Linear_Set(), Map())
+ doc.assign_states(Nil)
+ doc
+ }
+
+
+ // FIXME
+ var phase0: List[Text_Edit] = null
+ var phase1: Linear_Set[Command] = null
+ var phase2: Linear_Set[Command] = null
+ var phase3: List[Edit] = null
+
+
+
+ /** document edits **/
+
+ type Edit = (Option[Command], Option[Command])
+
+ def text_edits(session: Session, old_doc: Document, new_id: Isar_Document.Document_ID,
+ edits: List[Text_Edit]): (List[Edit], Document) =
+ {
+ require(old_doc.assignment.is_finished)
+
+
+ /* unparsed dummy commands */
+
+ def unparsed(source: String) =
+ new Command(null, List(Outer_Lex.Token(Outer_Lex.Token_Kind.UNPARSED, source)))
+
+ def is_unparsed(command: Command) = command.id == null
+
+ assert(!old_doc.commands.exists(is_unparsed)) // FIXME remove
+
+
+ /* phase 1: edit individual command source */
+
+ def edit_text(eds: List[Text_Edit], commands: Linear_Set[Command]): Linear_Set[Command] =
+ {
+ eds match {
+ case e :: es =>
+ command_starts(commands).find { // FIXME relative search!
+ case (cmd, cmd_start) =>
+ e.can_edit(cmd.source, cmd_start) || e.is_insert && e.start == cmd_start + cmd.length
+ } match {
+ case Some((cmd, cmd_start)) if e.can_edit(cmd.source, cmd_start) =>
+ val (rest, text) = e.edit(cmd.source, cmd_start)
+ val new_commands = commands.insert_after(Some(cmd), unparsed(text)) - cmd
+ edit_text(rest.toList ::: es, new_commands)
+
+ case Some((cmd, cmd_start)) =>
+ edit_text(es, commands.insert_after(Some(cmd), unparsed(e.text)))
+
+ case None =>
+ require(e.is_insert && e.start == 0)
+ edit_text(es, commands.insert_after(None, unparsed(e.text)))
+ }
+ case Nil => commands
+ }
+ }
+
+
+ /* phase 2: recover command spans */
+
+ def parse_spans(commands: Linear_Set[Command]): Linear_Set[Command] =
+ {
+ // FIXME relative search!
+ commands.elements.find(is_unparsed) match {
+ case Some(first_unparsed) =>
+ val prefix = commands.prev(first_unparsed)
+ val body = commands.elements(first_unparsed).takeWhile(is_unparsed).toList
+ val suffix = commands.next(body.last)
+
+ val sources = (prefix.toList ::: body ::: suffix.toList).flatMap(_.span.map(_.source))
+ val spans0 = Thy_Syntax.parse_spans(session.current_syntax.scan(sources.mkString))
+
+ val (before_edit, spans1) =
+ if (!spans0.isEmpty && Some(spans0.first) == prefix.map(_.span))
+ (prefix, spans0.tail)
+ else (if (prefix.isDefined) commands.prev(prefix.get) else None, spans0)
+
+ val (after_edit, spans2) =
+ if (!spans1.isEmpty && Some(spans1.last) == suffix.map(_.span))
+ (suffix, spans1.take(spans1.length - 1))
+ else (if (suffix.isDefined) commands.next(suffix.get) else None, spans1)
+
+ val inserted = spans2.map(span => new Command(session.create_id(), span))
+ val new_commands =
+ commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted)
+ parse_spans(new_commands)
+
+ case None => commands
+ }
+ }
+
+
+ /* phase 3: resulting document edits */
+
+ val result = Library.timeit("text_edits") {
+ val commands0 = old_doc.commands
+ val commands1 = Library.timeit("edit_text") { edit_text(edits, commands0) }
+ val commands2 = Library.timeit("parse_spans") { parse_spans(commands1) }
+
+ val removed_commands = commands0.elements.filter(!commands2.contains(_)).toList
+ val inserted_commands = commands2.elements.filter(!commands0.contains(_)).toList
+
+ val doc_edits =
+ removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
+ inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
+
+ val former_states = old_doc.assignment.join -- removed_commands
+
+ phase0 = edits
+ phase1 = commands1
+ phase2 = commands2
+ phase3 = doc_edits
+
+ (doc_edits, new Document(new_id, commands2, former_states))
+ }
+ result
+ }
+}
+
+
+class Document(
+ val id: Isar_Document.Document_ID,
+ val commands: Linear_Set[Command],
+ former_states: Map[Command, Command])
+{
+ /* command ranges */
+
+ def command_starts: Iterator[(Command, Int)] = Document.command_starts(commands)
+
+ def command_start(cmd: Command): Option[Int] =
+ command_starts.find(_._1 == cmd).map(_._2)
+
+ def command_range(i: Int): Iterator[(Command, Int)] =
+ command_starts dropWhile { case (cmd, start) => start + cmd.length <= i }
+
+ def command_range(i: Int, j: Int): Iterator[(Command, Int)] =
+ command_range(i) takeWhile { case (_, start) => start < j }
+
+ def command_at(i: Int): Option[(Command, Int)] =
+ {
+ val range = command_range(i)
+ if (range.hasNext) Some(range.next) else None
+ }
+
+
+ /* command state assignment */
+
+ val assignment = Future.promise[Map[Command, Command]]
+ def await_assignment { assignment.join }
+
+ @volatile private var tmp_states = former_states
+ private val time0 = System.currentTimeMillis
+
+ def assign_states(new_states: List[(Command, Command)])
+ {
+ assignment.fulfill(tmp_states ++ new_states)
+ tmp_states = Map()
+ System.err.println("assign_states: " + (System.currentTimeMillis - time0) + " ms elapsed time")
+ }
+
+ def current_state(cmd: Command): Option[State] =
+ {
+ require(assignment.is_finished)
+ (assignment.join).get(cmd).map(_.current_state)
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/markup_node.scala Mon Jan 11 23:11:31 2010 +0100
@@ -0,0 +1,111 @@
+/*
+ * Document markup nodes, with connection to Swing tree model
+ *
+ * @author Fabian Immler, TU Munich
+ * @author Makarius
+ */
+
+package isabelle
+
+
+import javax.swing.tree.DefaultMutableTreeNode
+
+
+
+class Markup_Node(val start: Int, val stop: Int, val info: Any)
+{
+ def fits_into(that: Markup_Node): Boolean =
+ that.start <= this.start && this.stop <= that.stop
+}
+
+
+class Markup_Tree(val node: Markup_Node, val branches: List[Markup_Tree])
+{
+ def set_branches(bs: List[Markup_Tree]): Markup_Tree = new Markup_Tree(node, bs)
+
+ private def add(branch: Markup_Tree) = // FIXME avoid sort
+ set_branches((branch :: branches) sort ((a, b) => a.node.start < b.node.start))
+
+ private def remove(bs: List[Markup_Tree]) = set_branches(branches -- bs)
+
+ def + (new_tree: Markup_Tree): Markup_Tree =
+ {
+ val new_node = new_tree.node
+ if (new_node fits_into node) {
+ var inserted = false
+ val new_branches =
+ branches.map(branch =>
+ if ((new_node fits_into branch.node) && !inserted) {
+ inserted = true
+ branch + new_tree
+ }
+ else branch)
+ if (!inserted) {
+ // new_tree did not fit into children of this
+ // -> insert between this and its branches
+ val fitting = branches filter(_.node fits_into new_node)
+ (this remove fitting) add ((new_tree /: fitting)(_ + _))
+ }
+ else set_branches(new_branches)
+ }
+ else {
+ System.err.println("ignored nonfitting markup: " + new_node)
+ this
+ }
+ }
+
+ def flatten: List[Markup_Node] =
+ {
+ var next_x = node.start
+ if (branches.isEmpty) List(this.node)
+ else {
+ val filled_gaps =
+ for {
+ child <- branches
+ markups =
+ if (next_x < child.node.start)
+ new Markup_Node(next_x, child.node.start, node.info) :: child.flatten
+ else child.flatten
+ update = (next_x = child.node.stop)
+ markup <- markups
+ } yield markup
+ if (next_x < node.stop)
+ filled_gaps + new Markup_Node(next_x, node.stop, node.info)
+ else filled_gaps
+ }
+ }
+}
+
+
+class Markup_Text(val markup: List[Markup_Tree], val content: String)
+{
+ private lazy val root =
+ new Markup_Tree(new Markup_Node(0, content.length, None), markup)
+
+ def + (new_tree: Markup_Tree): Markup_Text =
+ new Markup_Text((root + new_tree).branches, content)
+
+ def filter(pred: Markup_Node => Boolean): Markup_Text =
+ {
+ def filt(tree: Markup_Tree): List[Markup_Tree] =
+ {
+ val branches = tree.branches.flatMap(filt(_))
+ if (pred(tree.node)) List(tree.set_branches(branches))
+ else branches
+ }
+ new Markup_Text(markup.flatMap(filt(_)), content)
+ }
+
+ def flatten: List[Markup_Node] = markup.flatten(_.flatten)
+
+ def swing_tree(swing_node: Markup_Node => DefaultMutableTreeNode): DefaultMutableTreeNode =
+ {
+ def swing(tree: Markup_Tree): DefaultMutableTreeNode =
+ {
+ val node = swing_node(tree.node)
+ tree.branches foreach ((branch: Markup_Tree) => node.add(swing(branch)))
+ node
+ }
+ swing(root)
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/state.scala Mon Jan 11 23:11:31 2010 +0100
@@ -0,0 +1,117 @@
+/*
+ * Accumulating results from prover
+ *
+ * @author Fabian Immler, TU Munich
+ * @author Makarius
+ */
+
+package isabelle
+
+
+class State(
+ val command: Command,
+ val status: Command.Status.Value,
+ val rev_results: List[XML.Tree],
+ val markup_root: Markup_Text)
+{
+ def this(command: Command) =
+ this(command, Command.Status.UNPROCESSED, Nil, command.empty_markup)
+
+
+ /* content */
+
+ private def set_status(st: Command.Status.Value): State =
+ new State(command, st, rev_results, markup_root)
+
+ private def add_result(res: XML.Tree): State =
+ new State(command, status, res :: rev_results, markup_root)
+
+ private def add_markup(node: Markup_Tree): State =
+ new State(command, status, rev_results, markup_root + node)
+
+ lazy val results = rev_results.reverse
+
+
+ /* markup */
+
+ lazy val highlight: Markup_Text =
+ {
+ markup_root.filter(_.info match {
+ case Command.HighlightInfo(_) => true
+ case _ => false
+ })
+ }
+
+ private lazy val types: List[Markup_Node] =
+ markup_root.filter(_.info match {
+ case Command.TypeInfo(_) => true
+ case _ => false }).flatten
+
+ def type_at(pos: Int): Option[String] =
+ {
+ types.find(t => t.start <= pos && pos < t.stop) match {
+ case Some(t) =>
+ t.info match {
+ case Command.TypeInfo(ty) => Some(command.source(t.start, t.stop) + ": " + ty)
+ case _ => None
+ }
+ case None => None
+ }
+ }
+
+ private lazy val refs: List[Markup_Node] =
+ markup_root.filter(_.info match {
+ case Command.RefInfo(_, _, _, _) => true
+ case _ => false }).flatten
+
+ def ref_at(pos: Int): Option[Markup_Node] =
+ refs.find(t => t.start <= pos && pos < t.stop)
+
+
+ /* message dispatch */
+
+ def + (session: Session, message: XML.Tree): State =
+ {
+ val changed: State =
+ message match {
+ case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.STATUS) :: _, elems) =>
+ (this /: elems)((state, elem) =>
+ elem match {
+ case XML.Elem(Markup.UNPROCESSED, _, _) => state.set_status(Command.Status.UNPROCESSED)
+ 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.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!?
+ state.add_markup(
+ command.markup_node(begin.get - 1, end.get - 1, Command.TypeInfo(info)))
+ }
+ else if (kind == Markup.ML_REF) {
+ body match {
+ case List(XML.Elem(Markup.ML_DEF, atts, _)) =>
+ state.add_markup(command.markup_node(
+ begin.get - 1, end.get - 1,
+ Command.RefInfo(
+ Position.get_file(atts),
+ Position.get_line(atts),
+ Position.get_id(atts),
+ Position.get_offset(atts))))
+ case _ => state
+ }
+ }
+ else {
+ state.add_markup(
+ command.markup_node(begin.get - 1, end.get - 1, Command.HighlightInfo(kind)))
+ }
+ case _ =>
+ System.err.println("ignored status report: " + elem)
+ state
+ })
+ case _ => add_result(message)
+ }
+ if (!(this eq changed)) session.command_change.event(command)
+ changed
+ }
+}
--- a/src/Pure/Thy/text_edit.scala Mon Jan 11 16:45:02 2010 +0100
+++ b/src/Pure/Thy/text_edit.scala Mon Jan 11 23:11:31 2010 +0100
@@ -8,72 +8,44 @@
package isabelle
-sealed abstract class Text_Edit
+class Text_Edit(val is_insert: Boolean, val start: Int, val text: String)
{
- val start: Int
- def text: String
- def after(offset: Int): Int
- def before(offset: Int): Int
- def can_edit(string_length: Int, shift: Int): Boolean
- def edit(string: String, shift: Int): (Option[Text_Edit], String)
-}
+ override def toString =
+ (if (is_insert) "Insert(" else "Remove(") + (start, text).toString + ")"
-object Text_Edit
-{
/* transform offsets */
- private def after_insert(start: Int, text: String, offset: Int): Int =
- if (start <= offset) offset + text.length
- else offset
+ private def transform(do_insert: Boolean, offset: Int): Int =
+ if (offset < start) offset
+ else if (is_insert == do_insert) offset + text.length
+ else (offset - text.length) max start
- private def after_remove(start: Int, text: String, offset: Int): Int =
- if (start > offset) offset
- else (offset - text.length) max start
+ def after(offset: Int): Int = transform(true, offset)
+ def before(offset: Int): Int = transform(false, offset)
/* edit strings */
- private def insert(index: Int, text: String, string: String): String =
+ private def insert(index: Int, string: String): String =
string.substring(0, index) + text + string.substring(index)
private def remove(index: Int, count: Int, string: String): String =
string.substring(0, index) + string.substring(index + count)
-
- /* explicit edits */
-
- case class Insert(start: Int, text: String) extends Text_Edit
- {
- def after(offset: Int): Int = after_insert(start, text, offset)
- def before(offset: Int): Int = after_remove(start, text, offset)
-
- def can_edit(string_length: Int, shift: Int): Boolean =
- shift <= start && start <= shift + string_length
-
- def edit(string: String, shift: Int): (Option[Insert], String) =
- if (can_edit(string.length, shift)) (None, insert(start - shift, text, string))
- else (Some(this), string)
- }
+ def can_edit(string: String, shift: Int): Boolean =
+ shift <= start && start < shift + string.length
- case class Remove(start: Int, text: String) extends Text_Edit
- {
- def after(offset: Int): Int = after_remove(start, text, offset)
- def before(offset: Int): Int = after_insert(start, text, offset)
-
- def can_edit(string_length: Int, shift: Int): Boolean =
- shift <= start && start < shift + string_length
-
- def edit(string: String, shift: Int): (Option[Remove], String) =
- if (can_edit(string.length, shift)) {
- val index = start - shift
- val count = text.length min (string.length - index)
- val rest =
- if (count == text.length) None
- else Some(Remove(start, text.substring(count)))
- (rest, remove(index, count, string))
- }
- else (Some(this), string)
- }
+ def edit(string: String, shift: Int): (Option[Text_Edit], String) =
+ if (!can_edit(string, shift)) (Some(this), string)
+ else if (is_insert) (None, insert(start - shift, string))
+ else {
+ val index = start - shift
+ val count = text.length min (string.length - index)
+ val rest =
+ if (count == text.length) None
+ else Some(new Text_Edit(false, start, text.substring(count)))
+ (rest, remove(index, count, string))
+ }
}
--- a/src/Pure/Thy/thy_syntax.scala Mon Jan 11 16:45:02 2010 +0100
+++ b/src/Pure/Thy/thy_syntax.scala Mon Jan 11 23:11:31 2010 +0100
@@ -15,7 +15,7 @@
val command_span: Parser[Span] =
{
- val whitespace = token("white space", tok => tok.is_space || tok.is_comment)
+ val whitespace = token("white space", _.is_ignored)
val command = token("command keyword", _.is_command)
val body = not(rep(whitespace) ~ (command | eof)) ~> not_eof
command ~ rep(body) ^^ { case x ~ ys => x :: ys } | rep1(whitespace) | rep1(body)
--- a/src/Pure/build-jars Mon Jan 11 16:45:02 2010 +0100
+++ b/src/Pure/build-jars Mon Jan 11 23:11:31 2010 +0100
@@ -45,10 +45,16 @@
System/isabelle_syntax.scala
System/isabelle_system.scala
System/platform.scala
+ System/session.scala
System/session_manager.scala
System/standard_system.scala
+ Thy/change.scala
+ Thy/command.scala
Thy/completion.scala
+ Thy/document.scala
Thy/html.scala
+ Thy/markup_node.scala
+ Thy/state.scala
Thy/text_edit.scala
Thy/thy_header.scala
Thy/thy_syntax.scala
--- a/src/Pure/library.scala Mon Jan 11 16:45:02 2010 +0100
+++ b/src/Pure/library.scala Mon Jan 11 23:11:31 2010 +0100
@@ -55,12 +55,13 @@
/* timing */
- def timeit[A](e: => A) =
+ def timeit[A](message: String)(e: => A) =
{
val start = System.currentTimeMillis()
val result = Exn.capture(e)
val stop = System.currentTimeMillis()
- System.err.println((stop - start) + "ms elapsed time")
+ System.err.println(
+ (if (message.isEmpty) "" else message + ": ") + (stop - start) + "ms elapsed time")
Exn.release(result)
}
}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/README_BUILD Mon Jan 11 23:11:31 2010 +0100
@@ -0,0 +1,73 @@
+
+Requirements to build from sources
+==================================
+
+* Proper Java JRE/JDK from Sun, e.g. 1.6.0_17
+ http://java.sun.com/javase/downloads/index.jsp
+
+* Netbeans 6.7
+ http://www.netbeans.org/downloads/index.html
+
+* Scala for Netbeans: version 6.7v1 for NB 6.7
+ http://sourceforge.net/project/showfiles.php?group_id=192439&package_id=256544
+ http://blogtrader.net/dcaoyuan/category/NetBeans
+ http://wiki.netbeans.org/Scala
+
+* jEdit 4.3 (final)
+ http://www.jedit.org/
+
+ Netbeans Project "jEdit": install official sources as ./contrib/jEdit/.
+
+* jEdit plugins:
+ Netbeans Library "SideKick" = $HOME/.jedit/jars/SideKick.jar
+ Netbeans Library "ErrorList" = $HOME/.jedit/jars/ErrorList.jar
+ Netbeans Library "Hyperlinks" = $HOME/.jedit/jars/Hyperlinks.jar
+
+* Cobra Renderer 0.98.4
+ http://lobobrowser.org/cobra.jsp
+ Netbeans Library "Cobra-Renderer" = .../cobra.jar
+ Netbenas Library "Rhino-JavaScript" = .../js.jar
+
+* Isabelle/Pure Scala components
+ Netbeans Library "Isabelle-Pure" = ~~/lib/classes/Pure.jar
+
+
+Running the application within Netbeans
+=======================================
+
+* Project properties: add "Run" argument like
+ -noserver -nobackground -settings=/home/makarius/isabelle/isabelle-jedit/dist
+
+* The Isabelle environment is obtained automatically via
+ "$ISABELLE_HOME/bin/isabelle getenv", where ISABELLE_HOME is determined as follows:
+
+ (1) via regular Isabelle settings,
+ e.g. "isabelle env netbeans"
+
+ (2) or via ISABELLE_HOME from raw process environment,
+ e.g. "env ISABELLE_HOME=.../Isabelle netbeans"
+
+ (3) or via JVM system properties (cf. "Run / VM Options")
+ e.g. -Disabelle.home=.../Isabelle
+
+
+Misc notes
+==========
+
+- Netbeans config/Editors/Preferences/...-CustomPreferences.xml
+
+ <entry javaType="java.lang.Integer" name="caret-blink-rate" xml:space="preserve">
+ <value><![CDATA[0]]></value>
+ </entry>
+
+-----------------------------------------------------------------------
+To run jedit with remote debugging enabled, I use the following
+command: "java
+-agentlib:jdwp=transport=dt_socket,suspend=y,server=y,address=XXXX
+-jar jedit.jar"
+
+where XXXX is any open port number you wish. The above invocation
+works for Sun's JDK 5.0. There's an alternate incantation for earlier
+releases. (See
+http://java.sun.com/j2se/1.5.0/docs/guide/jpda/conninv.html)
+-----------------------------------------------------------------------
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/build.xml Mon Jan 11 23:11:31 2010 +0100
@@ -0,0 +1,102 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!-- You may freely edit this file. See commented blocks below for -->
+<!-- some examples of how to customize the build. -->
+<!-- (If you delete it and reopen the project it will be recreated.) -->
+<project name="Isabelle-jEdit" default="default" basedir=".">
+ <description>Builds, tests, and runs the project Isabelle-jEdit.</description>
+ <import file="nbproject/build-impl.xml"/>
+ <!--
+
+ There exist several targets which are by default empty and which can be
+ used for execution of your tasks. These targets are usually executed
+ before and after some main targets. They are:
+
+ -pre-init: called before initialization of project properties
+ -post-init: called after initialization of project properties
+ -pre-compile: called before javac compilation
+ -post-compile: called after javac compilation
+ -pre-compile-single: called before javac compilation of single file
+ -post-compile-single: called after javac compilation of single file
+ -pre-compile-test: called before javac compilation of JUnit tests
+ -post-compile-test: called after javac compilation of JUnit tests
+ -pre-compile-test-single: called before javac compilation of single JUnit test
+ -post-compile-test-single: called after javac compilation of single JUunit test
+ -pre-jar: called before JAR building
+ -post-jar: called after JAR building
+ -post-clean: called after cleaning build products
+
+ (Targets beginning with '-' are not intended to be called on their own.)
+
+ Example of inserting an obfuscator after compilation could look like this:
+
+ <target name="-post-compile">
+ <obfuscate>
+ <fileset dir="${build.classes.dir}"/>
+ </obfuscate>
+ </target>
+
+ For list of available properties check the imported
+ nbproject/build-impl.xml file.
+
+
+ Another way to customize the build is by overriding existing main targets.
+ The targets of interest are:
+
+ -init-macrodef-javac: defines macro for javac compilation
+ -init-macrodef-junit: defines macro for junit execution
+ -init-macrodef-debug: defines macro for class debugging
+ -init-macrodef-java: defines macro for class execution
+ -do-jar-with-manifest: JAR building (if you are using a manifest)
+ -do-jar-without-manifest: JAR building (if you are not using a manifest)
+ run: execution of project
+ -javadoc-build: Javadoc generation
+ test-report: JUnit report generation
+
+ An example of overriding the target for project execution could look like this:
+
+ <target name="run" depends="Isabelle-jEdit-impl.jar">
+ <exec dir="bin" executable="launcher.exe">
+ <arg file="${dist.jar}"/>
+ </exec>
+ </target>
+
+ Notice that the overridden target depends on the jar target and not only on
+ the compile target as the regular run target does. Again, for a list of available
+ properties which you can use, check the target you are overriding in the
+ nbproject/build-impl.xml file.
+
+ -->
+ <target name="run" depends="Isabelle-jEdit-impl.jar,Isabelle-jEdit-impl.run">
+ </target>
+ <target name="debug" depends="Isabelle-jEdit-impl.jar,Isabelle-jEdit-impl.debug">
+ </target>
+ <target name="-pre-jar">
+ <copy file="plugin/services.xml" todir="${build.classes.dir}" />
+ <copy file="plugin/dockables.xml" todir="${build.classes.dir}" />
+ <copy file="plugin/actions.xml" todir="${build.classes.dir}" />
+ <copy file="plugin/Isabelle.props" todir="${build.classes.dir}" />
+ </target>
+ <target name="-post-jar">
+ <!-- jars -->
+ <delete file="${dist.dir}/jars/lib/jEdit.jar" />
+ <move todir="${dist.dir}/jars">
+ <fileset dir="${dist.dir}/jars/lib" />
+ </move>
+ <copy file="${scala.library}" todir="${dist.dir}/jars" />
+ <copy file="${scala.lib}/scala-swing.jar" todir="${dist.dir}/jars" />
+ <!-- clean up -->
+ <delete dir="{dist.dir}/jars/lib" />
+ <!-- dist-template -->
+ <copy file="dist-template/properties/jedit.props" tofile="${dist.dir}/properties" />
+ <copy todir="${dist.dir}/modes">
+ <fileset dir="dist-template/modes" />
+ </copy>
+ <copy todir="${dist.dir}/modes" overwrite="true">
+ <fileset dir="${project.jEdit}/modes" />
+ </copy>
+ <replaceregexp byline="true" file="${dist.dir}/modes/catalog">
+ <regexp pattern='(^.*NAME="javacc".*$)'/>
+ <substitution expression="<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy"/>${line.separator}${line.separator}\1"/>
+ </replaceregexp>
+ </target>
+</project>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/contrib/jEdit/build-nb.xml Mon Jan 11 23:11:31 2010 +0100
@@ -0,0 +1,41 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<project name="jEdit">
+ <import file="./build.xml"/>
+ <property environment="env"/>
+
+ <target name="run" depends="compile">
+ <java classname="org.gjt.sp.jedit.jEdit" classpath="./build/jEdit.jar" dir="./" fork="true">
+ <arg value="-noserver"/>
+ <arg value="-nobackground"/>
+ <arg value="-settings=${env.ISABELLE_HOME_USER}/jedit"/>
+ </java>
+ </target>
+
+ <target name="debug-nb" depends="compile">
+ <path id="cp" location="./build/jEdit.jar" />
+
+ <nbjpdastart addressproperty="jpda.address" name="jEdit" transport="dt_socket">
+ <classpath refid="cp"/>
+ </nbjpdastart>
+
+ <java classname="org.gjt.sp.jedit.jEdit" classpathref="cp" fork="true" dir="./">
+ <jvmarg value="-Xdebug"/>
+ <jvmarg value="-Xrunjdwp:transport=dt_socket,address=${jpda.address}"/>
+ </java>
+ </target>
+
+ <target name="profile-nb" depends="compile">
+ <fail unless="netbeans.home">This target can only run inside the NetBeans IDE.</fail>
+
+ <path id="cp" location="./build/jEdit.jar" />
+
+ <nbprofiledirect>
+ <classpath refid="cp"/>
+ </nbprofiledirect>
+
+ <java classname="org.gjt.sp.jedit.jEdit" fork="true" logError="yes" dir="." classpathref="cp">
+ <classpath refid="cp"/>
+ <jvmarg value="${profiler.info.jvmargs.agent}"/>
+ </java>
+ </target>
+</project>
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/contrib/jEdit/nbproject/project.xml Mon Jan 11 23:11:31 2010 +0100
@@ -0,0 +1,118 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<project xmlns="http://www.netbeans.org/ns/project/1">
+ <type>org.netbeans.modules.ant.freeform</type>
+ <configuration>
+ <general-data xmlns="http://www.netbeans.org/ns/freeform-project/1">
+ <name>jEdit</name>
+ </general-data>
+ <general-data xmlns="http://www.netbeans.org/ns/freeform-project/2">
+ <!-- Do not use Project Properties customizer when editing this file manually. -->
+ <name>jEdit</name>
+ <properties>
+ <property name="ant.script">build-nb.xml</property>
+ </properties>
+ <folders>
+ <source-folder>
+ <label>jEdit</label>
+ <location>.</location>
+ <encoding>UTF-8</encoding>
+ </source-folder>
+ <source-folder>
+ <label>Source Packages</label>
+ <type>java</type>
+ <location>.</location>
+ <excludes>build/** doc/** icons/** macros/** modes/** package-files/**</excludes>
+ <encoding>UTF-8</encoding>
+ </source-folder>
+ </folders>
+ <ide-actions>
+ <action name="build">
+ <script>${ant.script}</script>
+ <target>build</target>
+ </action>
+ <action name="clean">
+ <script>${ant.script}</script>
+ <target>clean</target>
+ </action>
+ <action name="javadoc">
+ <script>${ant.script}</script>
+ <target>docs-javadoc</target>
+ </action>
+ <action name="run">
+ <script>${ant.script}</script>
+ <target>run</target>
+ </action>
+ <action name="rebuild">
+ <script>${ant.script}</script>
+ <target>clean</target>
+ <target>build</target>
+ </action>
+ <action name="debug">
+ <script>build-nb.xml</script>
+ <target>debug-nb</target>
+ </action>
+ </ide-actions>
+ <export>
+ <type>jar</type>
+ <location>build/jEdit.jar</location>
+ <script>${ant.script}</script>
+ <build-target>build</build-target>
+ </export>
+ <view>
+ <items>
+ <source-folder style="packages">
+ <label>Source Packages</label>
+ <location>.</location>
+ <excludes>build/** doc/** icons/** macros/** modes/** package-files/**</excludes>
+ </source-folder>
+ <source-file>
+ <location>${ant.script}</location>
+ </source-file>
+ </items>
+ <context-menu>
+ <ide-action name="build"/>
+ <ide-action name="rebuild"/>
+ <ide-action name="clean"/>
+ <ide-action name="javadoc"/>
+ <ide-action name="run"/>
+ <ide-action name="debug"/>
+ </context-menu>
+ </view>
+ <subprojects/>
+ </general-data>
+ <java-data xmlns="http://www.netbeans.org/ns/freeform-project-java/1">
+ <compilation-unit>
+ <package-root>.</package-root>
+ <classpath mode="compile">.</classpath>
+ <built-to>build/jEdit.jar</built-to>
+ <source-level>1.5</source-level>
+ </compilation-unit>
+ </java-data>
+ <preferences xmlns="http://www.netbeans.org/ns/auxiliary-configuration-preferences/1">
+ <module name="org-netbeans-modules-editor-indent">
+ <node name="CodeStyle">
+ <property name="usedProfile" value="default"/>
+ <node name="project">
+ <property name="spaces-per-tab" value="2"/>
+ <property name="tab-size" value="2"/>
+ <property name="indent-shift-width" value="2"/>
+ <property name="text-limit-width" value="100"/>
+ <property name="expand-tabs" value="true"/>
+ </node>
+ </node>
+ <node name="text">
+ <node name="x-java">
+ <node name="CodeStyle">
+ <node name="project">
+ <property name="tab-size" value="4"/>
+ <property name="text-limit-width" value="100"/>
+ <property name="spaces-per-tab" value="2"/>
+ <property name="indent-shift-width" value="2"/>
+ </node>
+ </node>
+ </node>
+ </node>
+ </module>
+ </preferences>
+ </configuration>
+</project>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/dist-template/etc/settings Mon Jan 11 23:11:31 2010 +0100
@@ -0,0 +1,9 @@
+JEDIT_HOME="$COMPONENT"
+
+JEDIT_JAVA_OPTIONS="-Xms128m -Xmx512m -Xss2m"
+#JEDIT_JAVA_OPTIONS="-server -Xms128m -Xmx1024m -Xss4m"
+JEDIT_OPTIONS="-reuseview -noserver -nobackground"
+
+ISABELLE_JEDIT_OPTIONS="-m xsymbols -m no_brackets -m no_type_brackets"
+
+ISABELLE_TOOLS="$ISABELLE_TOOLS:$JEDIT_HOME/lib/Tools"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/dist-template/lib/Tools/jedit Mon Jan 11 23:11:31 2010 +0100
@@ -0,0 +1,117 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# DESCRIPTION: Isabelle/jEdit interface wrapper
+
+
+## diagnostics
+
+PRG="$(basename "$0")"
+
+usage()
+{
+ echo
+ echo "Usage: isabelle $PRG [OPTIONS] [FILES ...]"
+ echo
+ echo " Options are:"
+ echo " -J OPTION add JVM runtime option"
+ echo " (default JEDIT_JAVA_OPTIONS=$JEDIT_JAVA_OPTIONS)"
+ echo " -d enable debugger"
+ echo " -j OPTION add jEdit runtime option"
+ echo " (default JEDIT_OPTIONS=$JEDIT_OPTIONS)"
+ echo " -l NAME logic image name (default ISABELLE_LOGIC=$ISABELLE_LOGIC)"
+ echo " -m MODE add print mode for output"
+ echo
+ echo "Start jEdit with Isabelle plugin setup and opens theory FILES"
+ echo "(default ~/Scratch.thy)."
+ echo
+ exit 1
+}
+
+fail()
+{
+ echo "$1" >&2
+ exit 2
+}
+
+
+## process command line
+
+# options
+
+JEDIT_LOGIC="$ISABELLE_LOGIC"
+JEDIT_PRINT_MODE=""
+
+getoptions()
+{
+ OPTIND=1
+ while getopts "J:dj:l:m:" OPT
+ do
+ case "$OPT" in
+ J)
+ JAVA_ARGS["${#JAVA_ARGS[@]}"]="$OPTARG"
+ ;;
+ d)
+ JAVA_ARGS["${#JAVA_ARGS[@]}"]="-Xdebug"
+ JAVA_ARGS["${#JAVA_ARGS[@]}"]="-Xrunjdwp:transport=dt_socket,server=y,suspend=n"
+ ;;
+ j)
+ ARGS["${#ARGS[@]}"]="$OPTARG"
+ ;;
+ l)
+ JEDIT_LOGIC="$OPTARG"
+ ;;
+ m)
+ if [ -z "$JEDIT_PRINT_MODE" ]; then
+ JEDIT_PRINT_MODE="$OPTARG"
+ else
+ JEDIT_PRINT_MODE="$JEDIT_PRINT_MODE,$OPTARG"
+ fi
+ ;;
+ \?)
+ usage
+ ;;
+ esac
+ done
+}
+
+declare -a JAVA_ARGS; eval "JAVA_ARGS=($JEDIT_JAVA_OPTIONS)"
+[ -n "$SCALA_HOME" ] && JAVA_ARGS["${#JAVA_ARGS[@]}"]="-Dscala.home=$SCALA_HOME"
+
+declare -a ARGS; eval "ARGS=($JEDIT_OPTIONS)"
+
+declare -a OPTIONS; eval "OPTIONS=($ISABELLE_JEDIT_OPTIONS)"
+getoptions "${OPTIONS[@]}"
+
+getoptions "$@"
+shift $(($OPTIND - 1))
+
+
+# args
+
+if [ "$#" -eq 0 ]; then
+ ARGS["${#ARGS[@]}"]="Scratch.thy"
+else
+ while [ "$#" -gt 0 ]; do
+ ARGS["${#ARGS[@]}"]="$(jvmpath "$1")"
+ shift
+ done
+fi
+
+
+## main
+
+case "$JEDIT_LOGIC" in
+ /*)
+ ;;
+ */*)
+ JEDIT_LOGIC="$(pwd -P)/$JEDIT_LOGIC"
+ ;;
+esac
+
+export JEDIT_LOGIC JEDIT_PRINT_MODE
+
+exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" \
+ -jar "$(jvmpath "$JEDIT_HOME/jedit.jar")" \
+ "-settings=$(jvmpath "$ISABELLE_HOME_USER/jedit")" "${ARGS[@]}"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/dist-template/modes/isabelle-session.xml Mon Jan 11 23:11:31 2010 +0100
@@ -0,0 +1,41 @@
+<?xml version="1.0"?>
+<!DOCTYPE MODE SYSTEM "xmode.dtd">
+
+<!-- Isabelle session mode -->
+<MODE>
+ <PROPS>
+ <PROPERTY NAME="commentStart" VALUE="(*"/>
+ <PROPERTY NAME="commentEnd" VALUE="*)"/>
+ <PROPERTY NAME="noWordSep" VALUE="_'.?"/>
+ <PROPERTY NAME="unalignedOpenBrackets" VALUE="(" />
+ <PROPERTY NAME="unalignedCloseBrackets" VALUE=")" />
+ <PROPERTY NAME="tabSize" VALUE="2" />
+ <PROPERTY NAME="indentSize" VALUE="2" />
+ </PROPS>
+ <RULES IGNORE_CASE="FALSE" HIGHLIGHT_DIGITS="FALSE" ESCAPE="\">
+ <SPAN TYPE="COMMENT1">
+ <BEGIN>(*</BEGIN>
+ <END>*)</END>
+ </SPAN>
+ <SPAN TYPE="COMMENT3">
+ <BEGIN>{*</BEGIN>
+ <END>*}</END>
+ </SPAN>
+ <SPAN TYPE="LITERAL1">
+ <BEGIN>`</BEGIN>
+ <END>`</END>
+ </SPAN>
+ <SPAN TYPE="LITERAL3">
+ <BEGIN>"</BEGIN>
+ <END>"</END>
+ </SPAN>
+ <KEYWORDS>
+ <KEYWORD1>session</KEYWORD1>
+ <KEYWORD2>parent</KEYWORD2>
+ <KEYWORD2>imports</KEYWORD2>
+ <KEYWORD2>uses</KEYWORD2>
+ <KEYWORD2>options</KEYWORD2>
+ <KEYWORD2>dependencies</KEYWORD2>
+ </KEYWORDS>
+ </RULES>
+</MODE>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/dist-template/modes/isabelle.xml Mon Jan 11 23:11:31 2010 +0100
@@ -0,0 +1,43 @@
+<?xml version="1.0"?>
+<!DOCTYPE MODE SYSTEM "xmode.dtd">
+
+<!-- Isabelle theory mode -->
+<MODE>
+ <PROPS>
+ <PROPERTY NAME="commentStart" VALUE="(*"/>
+ <PROPERTY NAME="commentEnd" VALUE="*)"/>
+ <PROPERTY NAME="noWordSep" VALUE="_'.?"/>
+ <PROPERTY NAME="indentOpenBrackets" VALUE="{"/>
+ <PROPERTY NAME="indentCloseBrackets" VALUE="}"/>
+ <PROPERTY NAME="unalignedOpenBrackets" VALUE="(" />
+ <PROPERTY NAME="unalignedCloseBrackets" VALUE=")" />
+ <PROPERTY NAME="tabSize" VALUE="2" />
+ <PROPERTY NAME="indentSize" VALUE="2" />
+ </PROPS>
+ <RULES IGNORE_CASE="FALSE" HIGHLIGHT_DIGITS="FALSE" ESCAPE="\">
+ <SPAN TYPE="COMMENT1">
+ <BEGIN>(*</BEGIN>
+ <END>*)</END>
+ </SPAN>
+ <SPAN TYPE="COMMENT3">
+ <BEGIN>{*</BEGIN>
+ <END>*}</END>
+ </SPAN>
+ <SPAN TYPE="LITERAL1">
+ <BEGIN>`</BEGIN>
+ <END>`</END>
+ </SPAN>
+ <SPAN TYPE="LITERAL3">
+ <BEGIN>"</BEGIN>
+ <END>"</END>
+ </SPAN>
+ <KEYWORDS>
+ <KEYWORD2>header</KEYWORD2>
+ <KEYWORD1>theory</KEYWORD1>
+ <KEYWORD2>imports</KEYWORD2>
+ <KEYWORD2>uses</KEYWORD2>
+ <KEYWORD2>begin</KEYWORD2>
+ <KEYWORD2>end</KEYWORD2>
+ </KEYWORDS>
+ </RULES>
+</MODE>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/dist-template/properties/jedit.props Mon Jan 11 23:11:31 2010 +0100
@@ -0,0 +1,191 @@
+#jEdit properties
+buffer.deepIndent=false
+buffer.encoding=UTF-8-Isabelle
+buffer.indentSize=2
+buffer.lineSeparator=\n
+buffer.maxLineLen=100
+buffer.noTabs=true
+buffer.sidekick.keystroke-parse=true
+buffer.tabSize=2
+delete-line.shortcut=A+d
+delete.shortcut2=C+d
+encoding.opt-out.Big5-HKSCS=true
+encoding.opt-out.Big5=true
+encoding.opt-out.COMPOUND_TEXT=true
+encoding.opt-out.EUC-JP=true
+encoding.opt-out.EUC-KR=true
+encoding.opt-out.GB18030=true
+encoding.opt-out.GB2312=true
+encoding.opt-out.GBK=true
+encoding.opt-out.IBM-Thai=true
+encoding.opt-out.IBM00858=true
+encoding.opt-out.IBM01140=true
+encoding.opt-out.IBM01141=true
+encoding.opt-out.IBM01142=true
+encoding.opt-out.IBM01143=true
+encoding.opt-out.IBM01144=true
+encoding.opt-out.IBM01145=true
+encoding.opt-out.IBM01146=true
+encoding.opt-out.IBM01147=true
+encoding.opt-out.IBM01148=true
+encoding.opt-out.IBM01149=true
+encoding.opt-out.IBM037=true
+encoding.opt-out.IBM1026=true
+encoding.opt-out.IBM1047=true
+encoding.opt-out.IBM273=true
+encoding.opt-out.IBM277=true
+encoding.opt-out.IBM278=true
+encoding.opt-out.IBM280=true
+encoding.opt-out.IBM284=true
+encoding.opt-out.IBM285=true
+encoding.opt-out.IBM297=true
+encoding.opt-out.IBM420=true
+encoding.opt-out.IBM424=true
+encoding.opt-out.IBM437=true
+encoding.opt-out.IBM500=true
+encoding.opt-out.IBM775=true
+encoding.opt-out.IBM850=true
+encoding.opt-out.IBM852=true
+encoding.opt-out.IBM855=true
+encoding.opt-out.IBM857=true
+encoding.opt-out.IBM860=true
+encoding.opt-out.IBM861=true
+encoding.opt-out.IBM862=true
+encoding.opt-out.IBM863=true
+encoding.opt-out.IBM864=true
+encoding.opt-out.IBM865=true
+encoding.opt-out.IBM866=true
+encoding.opt-out.IBM868=true
+encoding.opt-out.IBM869=true
+encoding.opt-out.IBM870=true
+encoding.opt-out.IBM871=true
+encoding.opt-out.IBM918=true
+encoding.opt-out.ISO-2022-CN=true
+encoding.opt-out.ISO-2022-JP-2=true
+encoding.opt-out.ISO-2022-JP=true
+encoding.opt-out.ISO-2022-KR=true
+encoding.opt-out.ISO-8859-13=true
+encoding.opt-out.ISO-8859-2=true
+encoding.opt-out.ISO-8859-3=true
+encoding.opt-out.ISO-8859-4=true
+encoding.opt-out.ISO-8859-5=true
+encoding.opt-out.ISO-8859-6=true
+encoding.opt-out.ISO-8859-7=true
+encoding.opt-out.ISO-8859-8=true
+encoding.opt-out.ISO-8859-9=true
+encoding.opt-out.JIS_X0201=true
+encoding.opt-out.JIS_X0212-1990=true
+encoding.opt-out.KOI8-R=true
+encoding.opt-out.KOI8-U=true
+encoding.opt-out.Shift_JIS=true
+encoding.opt-out.TIS-620=true
+encoding.opt-out.UTF-16=true
+encoding.opt-out.UTF-16BE=true
+encoding.opt-out.UTF-16LE=true
+encoding.opt-out.UTF-32=true
+encoding.opt-out.UTF-32BE=true
+encoding.opt-out.UTF-32LE=true
+encoding.opt-out.X-UTF-32BE-BOM=true
+encoding.opt-out.X-UTF-32LE-BOM=true
+encoding.opt-out.windows-1250=true
+encoding.opt-out.windows-1251=true
+encoding.opt-out.windows-1253=true
+encoding.opt-out.windows-1254=true
+encoding.opt-out.windows-1255=true
+encoding.opt-out.windows-1256=true
+encoding.opt-out.windows-1257=true
+encoding.opt-out.windows-1258=true
+encoding.opt-out.windows-31j=true
+encoding.opt-out.x-Big5-Solaris=true
+encoding.opt-out.x-EUC-TW=true
+encoding.opt-out.x-IBM1006=true
+encoding.opt-out.x-IBM1025=true
+encoding.opt-out.x-IBM1046=true
+encoding.opt-out.x-IBM1097=true
+encoding.opt-out.x-IBM1098=true
+encoding.opt-out.x-IBM1112=true
+encoding.opt-out.x-IBM1122=true
+encoding.opt-out.x-IBM1123=true
+encoding.opt-out.x-IBM1124=true
+encoding.opt-out.x-IBM1381=true
+encoding.opt-out.x-IBM1383=true
+encoding.opt-out.x-IBM33722=true
+encoding.opt-out.x-IBM737=true
+encoding.opt-out.x-IBM834=true
+encoding.opt-out.x-IBM856=true
+encoding.opt-out.x-IBM874=true
+encoding.opt-out.x-IBM875=true
+encoding.opt-out.x-IBM921=true
+encoding.opt-out.x-IBM922=true
+encoding.opt-out.x-IBM930=true
+encoding.opt-out.x-IBM933=true
+encoding.opt-out.x-IBM935=true
+encoding.opt-out.x-IBM937=true
+encoding.opt-out.x-IBM939=true
+encoding.opt-out.x-IBM942=true
+encoding.opt-out.x-IBM942C=true
+encoding.opt-out.x-IBM943=true
+encoding.opt-out.x-IBM943C=true
+encoding.opt-out.x-IBM948=true
+encoding.opt-out.x-IBM949=true
+encoding.opt-out.x-IBM949C=true
+encoding.opt-out.x-IBM950=true
+encoding.opt-out.x-IBM964=true
+encoding.opt-out.x-IBM970=true
+encoding.opt-out.x-ISCII91=true
+encoding.opt-out.x-ISO-2022-CN-CNS=true
+encoding.opt-out.x-ISO-2022-CN-GB=true
+encoding.opt-out.x-JIS0208=true
+encoding.opt-out.x-JISAutoDetect=true
+encoding.opt-out.x-Johab=true
+encoding.opt-out.x-MS932_0213=true
+encoding.opt-out.x-MS950-HKSCS=true
+encoding.opt-out.x-MacArabic=true
+encoding.opt-out.x-MacCentralEurope=true
+encoding.opt-out.x-MacCroatian=true
+encoding.opt-out.x-MacCyrillic=true
+encoding.opt-out.x-MacDingbat=true
+encoding.opt-out.x-MacGreek=true
+encoding.opt-out.x-MacHebrew=true
+encoding.opt-out.x-MacIceland=true
+encoding.opt-out.x-MacRoman=true
+encoding.opt-out.x-MacRomania=true
+encoding.opt-out.x-MacSymbol=true
+encoding.opt-out.x-MacThai=true
+encoding.opt-out.x-MacTurkish=true
+encoding.opt-out.x-MacUkraine=true
+encoding.opt-out.x-PCK=true
+encoding.opt-out.x-SJIS_0213=true
+encoding.opt-out.x-UTF-16LE-BOM=true
+encoding.opt-out.x-euc-jp-linux=true
+encoding.opt-out.x-eucJP-Open=true
+encoding.opt-out.x-iso-8859-11=true
+encoding.opt-out.x-mswin-936=true
+encoding.opt-out.x-windows-50220=true
+encoding.opt-out.x-windows-50221=true
+encoding.opt-out.x-windows-874=true
+encoding.opt-out.x-windows-949=true
+encoding.opt-out.x-windows-950=true
+encoding.opt-out.x-windows-iso2022jp=true
+encodingDetectors=BOM XML-PI buffer-local-property
+fallbackEncodings=UTF-8 ISO-8859-15 US-ASCII
+firstTime=false
+isabelle-protocol.dock-position=bottom
+isabelle-results.dock-position=bottom
+isabelle.activate.shortcut=CS+ENTER
+mode.isabelle.sidekick.showStatusWindow.label=true
+sidekick-tree.dock-position=right
+sidekick.buffer-save-parse=true
+sidekick.complete-delay=300
+tip.show=false
+view.antiAlias=standard
+view.blockCaret=true
+view.caretBlink=false
+view.eolMarkers=false
+view.extendedState=0
+view.font=IsabelleText
+view.fontsize=18
+view.fracFontMetrics=false
+view.gutter.fontsize=12
+view.middleMousePaste=true
+view.showToolbar=false
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/makedist Mon Jan 11 23:11:31 2010 +0100
@@ -0,0 +1,98 @@
+#!/usr/bin/env bash
+#
+# makedist -- make Isabelle/jEdit distribution
+
+## self references
+
+PRG=$(basename "$0")
+THIS=$(cd "$(dirname "$0")"; pwd)
+SUPER=$(cd "$THIS/.."; pwd)
+
+
+## diagnostics
+
+JEDIT_HOME="/home/isajedit/jedit-orig/4.3pre17"
+
+function usage()
+{
+ echo
+ echo "Usage: $PRG [OPTIONS]"
+ echo
+ echo " Options are:"
+ echo " -j DIR specify original jEdit distribution"
+ echo " (default: $JEDIT_HOME)"
+ echo
+ echo " Produce Isabelle/jEdit distribution from Netbeans build"
+ echo " in $THIS/dist"
+ echo
+ exit 1
+}
+
+fail()
+{
+ echo "$1" >&2
+ exit 2
+}
+
+
+## process command line
+
+# options
+
+while getopts "j:s:" OPT
+do
+ case "$OPT" in
+ j)
+ JEDIT_HOME="$OPTARG"
+ ;;
+ \?)
+ usage
+ ;;
+ esac
+done
+
+shift $(($OPTIND - 1))
+
+
+# args
+
+[ "$#" -ne 0 ] && usage
+
+
+## main
+
+cd "$THIS/dist" || fail "Bad directory: $THIS/dist"
+
+
+# target name
+
+VERSION=$(basename "$JEDIT_HOME")
+JEDIT="jedit-${VERSION}"
+
+rm -rf "$JEDIT" jedit
+mkdir "$JEDIT"
+ln -s "$JEDIT" jedit
+
+
+# copy stuff
+
+[ "$JEDIT_HOME/jedit.jar" ] || fail "Bad original jEdit directory: $JEDIT_HOME"
+cp -R "$JEDIT_HOME/." "$JEDIT/."
+rm -rf "$JEDIT/jEdit" "$JEDIT/build-support"
+
+mkdir -p "$JEDIT/jars"
+cp -R jars/. "$JEDIT/jars/."
+
+cp -R "$THIS/dist-template/." "$JEDIT/."
+
+perl -i -e 'while (<>) { if (m/NAME="javacc"/) {
+ print qq,<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy"/>\n\n,;
+ print qq,<MODE NAME="isabelle-session" FILE="isabelle-session.xml" FILE_NAME_GLOB="session.root"/>\n\n,; }
+ print; }' "$JEDIT/modes/catalog"
+
+
+# build archive
+
+echo "${JEDIT}.tar.gz"
+tar czf "${JEDIT}.tar.gz" "$JEDIT" jedit
+ln -sf "${JEDIT}.tar.gz" jedit.tar.gz
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/manifest.mf Mon Jan 11 23:11:31 2010 +0100
@@ -0,0 +1,3 @@
+Manifest-Version: 1.0
+X-COMMENT: Main-Class will be added automatically by build
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/nbproject/build-impl.xml Mon Jan 11 23:11:31 2010 +0100
@@ -0,0 +1,709 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!--
+*** GENERATED FROM project.xml - DO NOT EDIT ***
+*** EDIT ../build.xml INSTEAD ***
+
+For the purpose of easier reading the script
+is divided into following sections:
+
+ - initialization
+ - compilation
+ - jar
+ - execution
+ - debugging
+ - javadoc
+ - junit compilation
+ - junit execution
+ - junit debugging
+ - applet
+ - cleanup
+
+
+ -->
+<project xmlns:jaxrpc="http://www.netbeans.org/ns/scala-project/jax-rpc" xmlns:scalaProject1="http://www.netbeans.org/ns/scala-project/1" basedir=".." default="default" name="Isabelle-jEdit-impl">
+ <target depends="test,jar,javadoc" description="Build and test whole project." name="default"/>
+ <!--
+ ======================
+ INITIALIZATION SECTION
+ ======================
+ -->
+ <target name="-pre-init">
+ <!-- Empty placeholder for easier customization. -->
+ <!-- You can override this target in the ../build.xml file. -->
+ </target>
+ <target depends="-pre-init" name="-init-private">
+ <property file="nbproject/private/config.properties"/>
+ <property file="nbproject/private/configs/${config}.properties"/>
+ <property file="nbproject/private/private.properties"/>
+ <property environment="env"/>
+ <condition property="scala.home" value="${env.SCALA_HOME}">
+ <isset property="env.SCALA_HOME"/>
+ </condition>
+ <fail unless="scala.home">
+You must set SCALA_HOME or environment property and append "-J-Dscala.home=scalahomepath"
+property to the end of "netbeans_default_options" in NetBeansInstallationPath/etc/netbeans.conf to point to
+Scala installation directory.
+ </fail>
+ <property name="scala.compiler" value="${scala.home}/lib/scala-compiler.jar"/>
+ <property name="scala.library" value="${scala.home}/lib/scala-library.jar"/>
+ <property name="scala.lib" value="${scala.home}/lib"/>
+ <taskdef resource="scala/tools/ant/antlib.xml">
+ <classpath>
+ <pathelement location="${scala.compiler}"/>
+ <pathelement location="${scala.library}"/>
+ </classpath>
+ </taskdef>
+ <chmod dir="${scala.home}/bin" includes="**/*" perm="u+rx"/>
+ </target>
+ <target depends="-pre-init,-init-private" name="-init-user">
+ <property file="${user.properties.file}"/>
+ <!-- The two properties below are usually overridden -->
+ <!-- by the active platform. Just a fallback. -->
+ <property name="default.javac.source" value="1.4"/>
+ <property name="default.javac.target" value="1.4"/>
+ </target>
+ <target depends="-pre-init,-init-private,-init-user" name="-init-project">
+ <property file="nbproject/configs/${config}.properties"/>
+ <property file="nbproject/project.properties"/>
+ </target>
+ <target depends="-pre-init,-init-private,-init-user,-init-project,-init-macrodef-property" name="-do-init">
+ <available file="${manifest.file}" property="manifest.available"/>
+ <condition property="manifest.available+main.class">
+ <and>
+ <isset property="manifest.available"/>
+ <isset property="main.class"/>
+ <not>
+ <equals arg1="${main.class}" arg2="" trim="true"/>
+ </not>
+ </and>
+ </condition>
+ <condition property="manifest.available+main.class+mkdist.available">
+ <and>
+ <istrue value="${manifest.available+main.class}"/>
+ <isset property="libs.CopyLibs.classpath"/>
+ </and>
+ </condition>
+ <condition property="have.tests">
+ <or/>
+ </condition>
+ <condition property="have.sources">
+ <or>
+ <available file="${src.dir}"/>
+ </or>
+ </condition>
+ <condition property="netbeans.home+have.tests">
+ <and>
+ <isset property="netbeans.home"/>
+ <isset property="have.tests"/>
+ </and>
+ </condition>
+ <condition property="no.javadoc.preview">
+ <and>
+ <isset property="javadoc.preview"/>
+ <isfalse value="${javadoc.preview}"/>
+ </and>
+ </condition>
+ <property name="run.jvmargs" value=""/>
+ <property name="javac.compilerargs" value=""/>
+ <property name="work.dir" value="${basedir}"/>
+ <condition property="no.deps">
+ <and>
+ <istrue value="${no.dependencies}"/>
+ </and>
+ </condition>
+ <property name="javac.debug" value="true"/>
+ <property name="javadoc.preview" value="true"/>
+ <property name="application.args" value=""/>
+ <property name="source.encoding" value="${file.encoding}"/>
+ <condition property="javadoc.encoding.used" value="${javadoc.encoding}">
+ <and>
+ <isset property="javadoc.encoding"/>
+ <not>
+ <equals arg1="${javadoc.encoding}" arg2=""/>
+ </not>
+ </and>
+ </condition>
+ <property name="javadoc.encoding.used" value="${source.encoding}"/>
+ <property name="includes" value="**"/>
+ <property name="excludes" value=""/>
+ <property name="do.depend" value="false"/>
+ <condition property="do.depend.true">
+ <istrue value="${do.depend}"/>
+ </condition>
+ <condition else="" property="javac.compilerargs.jaxws" value="-Djava.endorsed.dirs='${jaxws.endorsed.dir}'">
+ <and>
+ <isset property="jaxws.endorsed.dir"/>
+ <available file="nbproject/jaxws-build.xml"/>
+ </and>
+ </condition>
+ </target>
+ <target name="-post-init">
+ <!-- Empty placeholder for easier customization. -->
+ <!-- You can override this target in the ../build.xml file. -->
+ </target>
+ <target depends="-pre-init,-init-private,-init-user,-init-project,-do-init" name="-init-check">
+ <fail unless="src.dir">Must set src.dir</fail>
+ <fail unless="build.dir">Must set build.dir</fail>
+ <fail unless="dist.dir">Must set dist.dir</fail>
+ <fail unless="build.classes.dir">Must set build.classes.dir</fail>
+ <fail unless="dist.javadoc.dir">Must set dist.javadoc.dir</fail>
+ <fail unless="build.test.classes.dir">Must set build.test.classes.dir</fail>
+ <fail unless="build.test.results.dir">Must set build.test.results.dir</fail>
+ <fail unless="build.classes.excludes">Must set build.classes.excludes</fail>
+ <fail unless="dist.jar">Must set dist.jar</fail>
+ </target>
+ <target name="-init-macrodef-property">
+ <macrodef name="property" uri="http://www.netbeans.org/ns/scala-project/1">
+ <attribute name="name"/>
+ <attribute name="value"/>
+ <sequential>
+ <property name="@{name}" value="${@{value}}"/>
+ </sequential>
+ </macrodef>
+ </target>
+ <target name="-init-macrodef-javac">
+ <macrodef name="javac" uri="http://www.netbeans.org/ns/scala-project/1">
+ <attribute default="${src.dir}" name="srcdir"/>
+ <attribute default="${build.classes.dir}" name="destdir"/>
+ <attribute default="${javac.classpath}" name="classpath"/>
+ <attribute default="${includes}" name="includes"/>
+ <attribute default="${excludes}" name="excludes"/>
+ <attribute default="${javac.debug}" name="debug"/>
+ <attribute default="" name="sourcepath"/>
+ <element name="customize" optional="true"/>
+ <sequential>
+ <javac debug="@{debug}" deprecation="${javac.deprecation}" destdir="@{destdir}" encoding="${source.encoding}" excludes="@{excludes}" includeantruntime="false" includes="@{includes}" source="${javac.source}" sourcepath="@{sourcepath}" srcdir="@{srcdir}" target="${javac.target}">
+ <classpath>
+ <path path="@{classpath}"/>
+ <fileset dir="${scala.lib}">
+ <include name="**/*.jar"/>
+ </fileset>
+ </classpath>
+ <compilerarg line="${javac.compilerargs} ${javac.compilerargs.jaxws}"/>
+ <customize/>
+ </javac>
+ </sequential>
+ </macrodef>
+ <macrodef name="depend" uri="http://www.netbeans.org/ns/scala-project/1">
+ <attribute default="${src.dir}" name="srcdir"/>
+ <attribute default="${build.classes.dir}" name="destdir"/>
+ <attribute default="${javac.classpath}" name="classpath"/>
+ <sequential>
+ <depend cache="${build.dir}/depcache" destdir="@{destdir}" excludes="${excludes}" includes="${includes}" srcdir="@{srcdir}">
+ <classpath>
+ <path path="@{classpath}"/>
+ </classpath>
+ </depend>
+ </sequential>
+ </macrodef>
+ <macrodef name="force-recompile" uri="http://www.netbeans.org/ns/scala-project/1">
+ <attribute default="${build.classes.dir}" name="destdir"/>
+ <sequential>
+ <fail unless="javac.includes">Must set javac.includes</fail>
+ <pathconvert pathsep="," property="javac.includes.binary">
+ <path>
+ <filelist dir="@{destdir}" files="${javac.includes}"/>
+ </path>
+ <globmapper from="*.java" to="*.class"/>
+ </pathconvert>
+ <delete>
+ <files includes="${javac.includes.binary}"/>
+ </delete>
+ </sequential>
+ </macrodef>
+ </target>
+ <target name="-init-macrodef-scalac">
+ <macrodef name="scalac" uri="http://www.netbeans.org/ns/scala-project/1">
+ <attribute default="${src.dir}" name="srcdir"/>
+ <attribute default="${build.classes.dir}" name="destdir"/>
+ <attribute default="${javac.classpath}" name="classpath"/>
+ <attribute default="${includes}" name="includes"/>
+ <attribute default="${excludes}" name="excludes"/>
+ <attribute default="${javac.compilerargs}" name="addparams"/>
+ <attribute default="" name="sourcepath"/>
+ <element name="customize" optional="true"/>
+ <sequential>
+ <fsc addparams="@{addparams}" destdir="@{destdir}" encoding="${source.encoding}" excludes="@{excludes}" includes="@{includes}" sourcepath="@{sourcepath}" srcdir="@{srcdir}" target="jvm-${javac.target}">
+ <classpath>
+ <path path="@{classpath}"/>
+ <fileset dir="${scala.lib}">
+ <include name="**/*.jar"/>
+ </fileset>
+ </classpath>
+ <customize/>
+ </fsc>
+ </sequential>
+ </macrodef>
+ <macrodef name="depend" uri="http://www.netbeans.org/ns/scala-project/1">
+ <attribute default="${src.dir}" name="srcdir"/>
+ <attribute default="${build.classes.dir}" name="destdir"/>
+ <attribute default="${javac.classpath}" name="classpath"/>
+ <sequential>
+ <depend cache="${build.dir}/depcache" destdir="@{destdir}" excludes="${excludes}" includes="${includes}" srcdir="@{srcdir}">
+ <classpath>
+ <path path="@{classpath}"/>
+ </classpath>
+ </depend>
+ </sequential>
+ </macrodef>
+ <macrodef name="force-recompile" uri="http://www.netbeans.org/ns/scala-project/1">
+ <attribute default="${build.classes.dir}" name="destdir"/>
+ <sequential>
+ <fail unless="javac.includes">Must set javac.includes</fail>
+ <pathconvert pathsep="," property="javac.includes.binary">
+ <path>
+ <filelist dir="@{destdir}" files="${javac.includes}"/>
+ </path>
+ <globmapper from="*.scala" to="*.class"/>
+ </pathconvert>
+ <delete>
+ <files includes="${javac.includes.binary}"/>
+ </delete>
+ </sequential>
+ </macrodef>
+ </target>
+ <target name="-init-macrodef-junit">
+ <macrodef name="junit" uri="http://www.netbeans.org/ns/scala-project/1">
+ <attribute default="${includes}" name="includes"/>
+ <attribute default="${excludes}" name="excludes"/>
+ <attribute default="**" name="testincludes"/>
+ <sequential>
+ <junit dir="${work.dir}" errorproperty="tests.failed" failureproperty="tests.failed" fork="true" showoutput="true">
+ <batchtest todir="${build.test.results.dir}">
+ <fileset dir="${build.test.classes.dir}" excludes="@{excludes},${excludes}" includes="@{includes}">
+ <filename name="@{testincludes}"/>
+ </fileset>
+ </batchtest>
+ <classpath>
+ <path path="${run.test.classpath}"/>
+ <fileset dir="${scala.lib}">
+ <include name="**/*.jar"/>
+ </fileset>
+ </classpath>
+ <syspropertyset>
+ <propertyref prefix="test-sys-prop."/>
+ <mapper from="test-sys-prop.*" to="*" type="glob"/>
+ </syspropertyset>
+ <formatter type="brief" usefile="false"/>
+ <formatter type="xml"/>
+ <jvmarg line="${run.jvmargs}"/>
+ </junit>
+ </sequential>
+ </macrodef>
+ </target>
+ <target name="-init-macrodef-nbjpda">
+ <macrodef name="nbjpdastart" uri="http://www.netbeans.org/ns/scala-project/1">
+ <attribute default="${main.class}" name="name"/>
+ <attribute default="${debug.classpath}" name="classpath"/>
+ <attribute default="" name="stopclassname"/>
+ <sequential>
+ <nbjpdastart addressproperty="jpda.address" name="@{name}" stopclassname="@{stopclassname}" transport="dt_socket">
+ <classpath>
+ <path path="@{classpath}"/>
+ </classpath>
+ </nbjpdastart>
+ </sequential>
+ </macrodef>
+ <macrodef name="nbjpdareload" uri="http://www.netbeans.org/ns/scala-project/1">
+ <attribute default="${build.classes.dir}" name="dir"/>
+ <sequential>
+ <nbjpdareload>
+ <fileset dir="@{dir}" includes="${fix.includes}*.class"/>
+ </nbjpdareload>
+ </sequential>
+ </macrodef>
+ </target>
+ <target name="-init-debug-args">
+ <property name="version-output" value="java version "${ant.java.version}"/>
+ <condition property="have-jdk-older-than-1.4">
+ <or>
+ <contains string="${version-output}" substring="java version "1.0"/>
+ <contains string="${version-output}" substring="java version "1.1"/>
+ <contains string="${version-output}" substring="java version "1.2"/>
+ <contains string="${version-output}" substring="java version "1.3"/>
+ </or>
+ </condition>
+ <condition else="-Xdebug" property="debug-args-line" value="-Xdebug -Xnoagent -Djava.compiler=none">
+ <istrue value="${have-jdk-older-than-1.4}"/>
+ </condition>
+ </target>
+ <target depends="-init-debug-args" name="-init-macrodef-debug">
+ <macrodef name="debug" uri="http://www.netbeans.org/ns/scala-project/1">
+ <attribute default="${main.class}" name="classname"/>
+ <attribute default="${debug.classpath}" name="classpath"/>
+ <element name="customize" optional="true"/>
+ <sequential>
+ <java classname="@{classname}" dir="${work.dir}" fork="true">
+ <jvmarg line="${debug-args-line}"/>
+ <jvmarg value="-Xrunjdwp:transport=dt_socket,address=${jpda.address}"/>
+ <jvmarg line="${run.jvmargs}"/>
+ <classpath>
+ <path path="@{classpath}"/>
+ <fileset dir="${scala.lib}">
+ <include name="**/*.jar"/>
+ </fileset>
+ </classpath>
+ <syspropertyset>
+ <propertyref prefix="run-sys-prop."/>
+ <mapper from="run-sys-prop.*" to="*" type="glob"/>
+ </syspropertyset>
+ <customize/>
+ </java>
+ </sequential>
+ </macrodef>
+ </target>
+ <target name="-init-macrodef-java">
+ <macrodef name="java" uri="http://www.netbeans.org/ns/scala-project/1">
+ <attribute default="${main.class}" name="classname"/>
+ <element name="customize" optional="true"/>
+ <sequential>
+ <java classname="@{classname}" dir="${work.dir}" fork="true">
+ <jvmarg line="${run.jvmargs}"/>
+ <classpath>
+ <path path="${run.classpath}"/>
+ <fileset dir="${scala.lib}">
+ <include name="**/*.jar"/>
+ </fileset>
+ </classpath>
+ <syspropertyset>
+ <propertyref prefix="run-sys-prop."/>
+ <mapper from="run-sys-prop.*" to="*" type="glob"/>
+ </syspropertyset>
+ <customize/>
+ </java>
+ </sequential>
+ </macrodef>
+ </target>
+ <target name="-init-presetdef-jar">
+ <presetdef name="jar" uri="http://www.netbeans.org/ns/scala-project/1">
+ <jar compress="${jar.compress}" jarfile="${dist.jar}">
+ <scalaProject1:fileset dir="${build.classes.dir}"/>
+ </jar>
+ </presetdef>
+ </target>
+ <target depends="-pre-init,-init-private ,-init-user,-init-project,-do-init,-post-init,-init-check,-init-macrodef-property,-init-macrodef-javac,-init-macrodef-scalac,-init-macrodef-junit,-init-macrodef-nbjpda,-init-macrodef-debug,-init-macrodef-java,-init-presetdef-jar" name="init"/>
+ <!--
+ ===================
+ COMPILATION SECTION
+ ===================
+ -->
+ <target depends="init" name="deps-jar" unless="no.deps">
+ <ant antfile="${project.jEdit}/build-nb.xml" inheritall="false" target="build"/>
+ </target>
+ <target depends="init,deps-jar" name="-pre-pre-compile">
+ <mkdir dir="${build.classes.dir}"/>
+ </target>
+ <target name="-pre-compile">
+ <!-- Empty placeholder for easier customization. -->
+ <!-- You can override this target in the ../build.xml file. -->
+ </target>
+ <target if="do.depend.true" name="-compile-depend">
+ <scalaProject1:depend/>
+ </target>
+ <target depends="init,deps-jar,-pre-pre-compile,-pre-compile,-compile-depend" if="have.sources" name="-do-compile">
+ <scalaProject1:scalac/>
+ <scalaProject1:javac/>
+ <copy todir="${build.classes.dir}">
+ <fileset dir="${src.dir}" excludes="${build.classes.excludes},${excludes} " includes="${includes}"/>
+ </copy>
+ </target>
+ <target name="-post-compile">
+ <!-- Empty placeholder for easier customization. -->
+ <!-- You can override this target in the ../build.xml file. -->
+ </target>
+ <target depends="init,deps-jar,-pre-pre-compile,-pre-compile,-do-compile,-post-compile" description="Compile project." name="compile"/>
+ <target name="-pre-compile-single">
+ <!-- Empty placeholder for easier customization. -->
+ <!-- You can override this target in the ../build.xml file. -->
+ </target>
+ <target depends="init,deps-jar,-pre-pre-compile" name="-do-compile-single">
+ <fail unless="javac.includes">Must select some files in the IDE or set javac.includes</fail>
+ <scalaProject1:force-recompile/>
+ <scalaProject1:scalac excludes="" includes="${javac.includes}" sourcepath="${src.dir}"/>
+ </target>
+ <target name="-post-compile-single">
+ <!-- Empty placeholder for easier customization. -->
+ <!-- You can override this target in the ../build.xml file. -->
+ </target>
+ <target depends="init,deps-jar,-pre-pre-compile,-pre-compile-single,-do-compile-single,-post-compile-single" name="compile-single"/>
+ <!--
+ ====================
+ JAR BUILDING SECTION
+ ====================
+ -->
+ <target depends="init" name="-pre-pre-jar">
+ <dirname file="${dist.jar}" property="dist.jar.dir"/>
+ <mkdir dir="${dist.jar.dir}"/>
+ </target>
+ <target name="-pre-jar">
+ <!-- Empty placeholder for easier customization. -->
+ <!-- You can override this target in the ../build.xml file. -->
+ </target>
+ <target depends="init,compile,-pre-pre-jar,-pre-jar" name="-do-jar-without-manifest" unless="manifest.available">
+ <scalaProject1:jar/>
+ </target>
+ <target depends="init,compile,-pre-pre-jar,-pre-jar" if="manifest.available" name="-do-jar-with-manifest" unless="manifest.available+main.class">
+ <scalaProject1:jar manifest="${manifest.file}"/>
+ </target>
+ <target depends="init,compile,-pre-pre-jar,-pre-jar" if="manifest.available+main.class" name="-do-jar-with-mainclass" unless="manifest.available+main.class+mkdist.available">
+ <scalaProject1:jar manifest="${manifest.file}">
+ <scalaProject1:manifest>
+ <scalaProject1:attribute name="Main-Class" value="${main.class}"/>
+ </scalaProject1:manifest>
+ </scalaProject1:jar>
+ <echo>To run this application from the command line without Ant, try:</echo>
+ <property location="${build.classes.dir}" name="build.classes.dir.resolved"/>
+ <property location="${dist.jar}" name="dist.jar.resolved"/>
+ <pathconvert property="run.classpath.with.dist.jar">
+ <path path="${run.classpath}"/>
+ <map from="${build.classes.dir.resolved}" to="${dist.jar.resolved}"/>
+ </pathconvert>
+ <echo>java -cp "${run.classpath.with.dist.jar}" ${main.class}
+ </echo>
+ </target>
+ <target depends="init,compile,-pre-pre-jar,-pre-jar" if="manifest.available+main.class+mkdist.available" name="-do-jar-with-libraries">
+ <property location="${build.classes.dir}" name="build.classes.dir.resolved"/>
+ <pathconvert property="run.classpath.without.build.classes.dir">
+ <path path="${run.classpath}"/>
+ <map from="${build.classes.dir.resolved}" to=""/>
+ </pathconvert>
+ <pathconvert pathsep=" " property="jar.classpath">
+ <path path="${run.classpath.without.build.classes.dir}"/>
+ <chainedmapper>
+ <flattenmapper/>
+ <globmapper from="*" to="lib/*"/>
+ </chainedmapper>
+ </pathconvert>
+ <taskdef classname="org.netbeans.modules.java.j2seproject.copylibstask.CopyLibs" classpath="${libs.CopyLibs.classpath}" name="copylibs"/>
+ <copylibs compress="${jar.compress}" jarfile="${dist.jar}" manifest="${manifest.file}" runtimeclasspath="${run.classpath.without.build.classes.dir}">
+ <fileset dir="${build.classes.dir}"/>
+ <manifest>
+ <attribute name="Main-Class" value="${main.class}"/>
+ <attribute name="Class-Path" value="${jar.classpath}"/>
+ </manifest>
+ </copylibs>
+ <echo>To run this application from the command line without Ant, try:</echo>
+ <property location="${dist.jar}" name="dist.jar.resolved"/>
+ <echo>java -jar "${dist.jar.resolved}"
+ </echo>
+ </target>
+ <target name="-post-jar">
+ <!-- Empty placeholder for easier customization. -->
+ <!-- You can override this target in the ../build.xml file. -->
+ </target>
+ <target depends="init,compile,-pre-jar,-do-jar-with-manifest,-do-jar-without-manifest,-do-jar-with-mainclass,-do-jar-with-libraries,-post-jar" description="Build JAR." name="jar"/>
+ <!--
+ =================
+ EXECUTION SECTION
+ =================
+ -->
+ <target depends="init,compile" description="Run a main class." name="run">
+ <scalaProject1:java>
+ <customize>
+ <arg line="${application.args}"/>
+ </customize>
+ </scalaProject1:java>
+ </target>
+ <target name="-do-not-recompile">
+ <property name="javac.includes.binary" value=""/>
+ </target>
+ <target depends="init,-do-not-recompile,compile-single" name="run-single">
+ <fail unless="run.class">Must select one file in the IDE or set run.class</fail>
+ <scalaProject1:java classname="${run.class}"/>
+ </target>
+ <!--
+ =================
+ DEBUGGING SECTION
+ =================
+ -->
+ <target depends="init" if="netbeans.home" name="-debug-start-debugger">
+ <scalaProject1:nbjpdastart name="${debug.class}"/>
+ </target>
+ <target depends="init,compile" name="-debug-start-debuggee">
+ <scalaProject1:debug>
+ <customize>
+ <arg line="${application.args}"/>
+ </customize>
+ </scalaProject1:debug>
+ </target>
+ <target depends="init,compile,-debug-start-debugger,-debug-start-debuggee" description="Debug project in IDE." if="netbeans.home" name="debug"/>
+ <target depends="init" if="netbeans.home" name="-debug-start-debugger-stepinto">
+ <scalaProject1:nbjpdastart stopclassname="${main.class}"/>
+ </target>
+ <target depends="init,compile,-debug-start-debugger-stepinto,-debug-start-debuggee" if="netbeans.home" name="debug-stepinto"/>
+ <target depends="init,compile-single" if="netbeans.home" name="-debug-start-debuggee-single">
+ <fail unless="debug.class">Must select one file in the IDE or set debug.class</fail>
+ <scalaProject1:debug classname="${debug.class}"/>
+ </target>
+ <target depends="init,-do-not-recompile,compile-single,-debug-start-debugger,-debug-start-debuggee-single" if="netbeans.home" name="debug-single"/>
+ <target depends="init" name="-pre-debug-fix">
+ <fail unless="fix.includes">Must set fix.includes</fail>
+ <property name="javac.includes" value="${fix.includes}.java"/>
+ </target>
+ <target depends="init,-pre-debug-fix,compile-single" if="netbeans.home" name="-do-debug-fix">
+ <scalaProject1:nbjpdareload/>
+ </target>
+ <target depends="init,-pre-debug-fix,-do-debug-fix" if="netbeans.home" name="debug-fix"/>
+ <!--
+ ===============
+ JAVADOC SECTION
+ ===============
+ -->
+ <target depends="init" name="-javadoc-build">
+ <mkdir dir="${dist.javadoc.dir}"/>
+ <javadoc additionalparam="${javadoc.additionalparam}" author="${javadoc.author}" charset="UTF-8" destdir="${dist.javadoc.dir}" docencoding="UTF-8" encoding="${javadoc.encoding.used}" failonerror="true" noindex="${javadoc.noindex}" nonavbar="${javadoc.nonavbar}" notree="${javadoc.notree}" private="${javadoc.private}" source="${javac.source}" splitindex="${javadoc.splitindex}" use="${javadoc.use}" useexternalfile="true" version="${javadoc.version}" windowtitle="${javadoc.windowtitle}">
+ <classpath>
+ <path path="${javac.classpath}"/>
+ </classpath>
+ <fileset dir="${src.dir}" excludes="${excludes}" includes="${includes}">
+ <filename name="**/*.java"/>
+ </fileset>
+ </javadoc>
+ </target>
+ <target depends="init,-javadoc-build" if="netbeans.home" name="-javadoc-browse" unless="no.javadoc.preview">
+ <nbbrowse file="${dist.javadoc.dir}/index.html"/>
+ </target>
+ <target depends="init,-javadoc-build,-javadoc-browse" description="Build Javadoc." name="javadoc"/>
+ <!--
+ =========================
+ JUNIT COMPILATION SECTION
+ =========================
+ -->
+ <target depends="init,compile" if="have.tests" name="-pre-pre-compile-test">
+ <mkdir dir="${build.test.classes.dir}"/>
+ </target>
+ <target name="-pre-compile-test">
+ <!-- Empty placeholder for easier customization. -->
+ <!-- You can override this target in the ../build.xml file. -->
+ </target>
+ <target if="do.depend.true" name="-compile-test-depend">
+ <scalaProject1:depend classpath="${javac.test.classpath}" destdir="${build.test.classes.dir}" srcdir=""/>
+ </target>
+ <target depends="init,compile,-pre-pre-compile-test,-pre-compile-test,-compile-test-depend" if="have.tests" name="-do-compile-test">
+ <scalaProject1:scalac classpath="${javac.test.classpath}" debug="true" destdir="${build.test.classes.dir}" srcdir=""/>
+ <copy todir="${build.test.classes.dir}"/>
+ </target>
+ <target name="-post-compile-test">
+ <!-- Empty placeholder for easier customization. -->
+ <!-- You can override this target in the ../build.xml file. -->
+ </target>
+ <target depends="init,compile,-pre-pre-compile-test,-pre-compile-test,-do-compile-test,-post-compile-test" name="compile-test"/>
+ <target name="-pre-compile-test-single">
+ <!-- Empty placeholder for easier customization. -->
+ <!-- You can override this target in the ../build.xml file. -->
+ </target>
+ <target depends="init,compile,-pre-pre-compile-test,-pre-compile-test-single" if="have.tests" name="-do-compile-test-single">
+ <fail unless="javac.includes">Must select some files in the IDE or set javac.includes</fail>
+ <scalaProject1:force-recompile destdir="${build.test.classes.dir}"/>
+ <scalaProject1:scalac classpath="${javac.test.classpath}" debug="true" destdir="${build.test.classes.dir}" excludes="" includes="${javac.includes}" sourcepath="" srcdir=""/>
+ <copy todir="${build.test.classes.dir}"/>
+ </target>
+ <target name="-post-compile-test-single">
+ <!-- Empty placeholder for easier customization. -->
+ <!-- You can override this target in the ../build.xml file. -->
+ </target>
+ <target depends="init,compile,-pre-pre-compile-test,-pre-compile-test-single,-do-compile-test-single,-post-compile-test-single" name="compile-test-single"/>
+ <!--
+ =======================
+ JUNIT EXECUTION SECTION
+ =======================
+ -->
+ <target depends="init" if="have.tests" name="-pre-test-run">
+ <mkdir dir="${build.test.results.dir}"/>
+ </target>
+ <target depends="init,compile-test,-pre-test-run" if="have.tests" name="-do-test-run">
+ <scalaProject1:junit testincludes="**/*Test.class"/>
+ </target>
+ <target depends="init,compile-test,-pre-test-run,-do-test-run" if="have.tests" name="-post-test-run">
+ <fail if="tests.failed">Some tests failed; see details above.</fail>
+ </target>
+ <target depends="init" if="have.tests" name="test-report"/>
+ <target depends="init" if="netbeans.home+have.tests" name="-test-browse"/>
+ <target depends="init,compile-test,-pre-test-run,-do-test-run,test-report,-post-test-run,-test-browse" description="Run unit tests." name="test"/>
+ <target depends="init" if="have.tests" name="-pre-test-run-single">
+ <mkdir dir="${build.test.results.dir}"/>
+ </target>
+ <target depends="init,compile-test-single,-pre-test-run-single" if="have.tests" name="-do-test-run-single">
+ <fail unless="test.includes">Must select some files in the IDE or set test.includes</fail>
+ <scalaProject1:junit excludes="" includes="${test.includes}"/>
+ </target>
+ <target depends="init,compile-test-single,-pre-test-run-single,-do-test-run-single" if="have.tests" name="-post-test-run-single">
+ <fail if="tests.failed">Some tests failed; see details above.</fail>
+ </target>
+ <target depends="init,-do-not-recompile,compile-test-single,-pre-test-run-single,-do-test-run-single,-post-test-run-single" description="Run single unit test." name="test-single"/>
+ <!--
+ =======================
+ JUNIT DEBUGGING SECTION
+ =======================
+ -->
+ <target depends="init,compile-test" if="have.tests" name="-debug-start-debuggee-test">
+ <fail unless="test.class">Must select one file in the IDE or set test.class</fail>
+ <property location="${build.test.results.dir}/TEST-${test.class}.xml" name="test.report.file"/>
+ <delete file="${test.report.file}"/>
+ <mkdir dir="${build.test.results.dir}"/>
+ <scalaProject1:debug classname="org.apache.tools.ant.taskdefs.optional.junit.JUnitTestRunner" classpath="${ant.home}/lib/ant.jar:${ant.home}/lib/ant-junit.jar:${debug.test.classpath}">
+ <customize>
+ <syspropertyset>
+ <propertyref prefix="test-sys-prop."/>
+ <mapper from="test-sys-prop.*" to="*" type="glob"/>
+ </syspropertyset>
+ <arg value="${test.class}"/>
+ <arg value="showoutput=true"/>
+ <arg value="formatter=org.apache.tools.ant.taskdefs.optional.junit.BriefJUnitResultFormatter"/>
+ <arg value="formatter=org.apache.tools.ant.taskdefs.optional.junit.XMLJUnitResultFormatter,${test.report.file}"/>
+ </customize>
+ </scalaProject1:debug>
+ </target>
+ <target depends="init,compile-test" if="netbeans.home+have.tests" name="-debug-start-debugger-test">
+ <scalaProject1:nbjpdastart classpath="${debug.test.classpath}" name="${test.class}"/>
+ </target>
+ <target depends="init,-do-not-recompile,compile-test-single,-debug-start-debugger-test,-debug-start-debuggee-test" name="debug-test"/>
+ <target depends="init,-pre-debug-fix,compile-test-single" if="netbeans.home" name="-do-debug-fix-test">
+ <scalaProject1:nbjpdareload dir="${build.test.classes.dir}"/>
+ </target>
+ <target depends="init,-pre-debug-fix,-do-debug-fix-test" if="netbeans.home" name="debug-fix-test"/>
+ <!--
+ =========================
+ APPLET EXECUTION SECTION
+ =========================
+ -->
+ <target depends="init,compile-single" name="run-applet">
+ <fail unless="applet.url">Must select one file in the IDE or set applet.url</fail>
+ <scalaProject1:java classname="sun.applet.AppletViewer">
+ <customize>
+ <arg value="${applet.url}"/>
+ </customize>
+ </scalaProject1:java>
+ </target>
+ <!--
+ =========================
+ APPLET DEBUGGING SECTION
+ =========================
+ -->
+ <target depends="init,compile-single" if="netbeans.home" name="-debug-start-debuggee-applet">
+ <fail unless="applet.url">Must select one file in the IDE or set applet.url</fail>
+ <scalaProject1:debug classname="sun.applet.AppletViewer">
+ <customize>
+ <arg value="${applet.url}"/>
+ </customize>
+ </scalaProject1:debug>
+ </target>
+ <target depends="init,compile-single,-debug-start-debugger,-debug-start-debuggee-applet" if="netbeans.home" name="debug-applet"/>
+ <!--
+ ===============
+ CLEANUP SECTION
+ ===============
+ -->
+ <target depends="init" name="deps-clean" unless="no.deps">
+ <ant antfile="${project.jEdit}/build-nb.xml" inheritall="false" target="clean"/>
+ </target>
+ <target depends="init" name="-do-clean">
+ <delete dir="${build.dir}"/>
+ <delete dir="${dist.dir}"/>
+ </target>
+ <target name="-post-clean">
+ <!-- Empty placeholder for easier customization. -->
+ <!-- You can override this target in the ../build.xml file. -->
+ </target>
+ <target depends="init,deps-clean,-do-clean,-post-clean" description="Clean build products." name="clean"/>
+</project>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/nbproject/genfiles.properties Mon Jan 11 23:11:31 2010 +0100
@@ -0,0 +1,8 @@
+build.xml.data.CRC32=d2379ac2
+build.xml.script.CRC32=2db9d955
+build.xml.stylesheet.CRC32=ca9d572e
+# This file is used by a NetBeans-based IDE to track changes in generated files such as build-impl.xml.
+# Do not edit this file. You may delete it but then the IDE will never regenerate such files for you.
+nbproject/build-impl.xml.data.CRC32=8f41dcce
+nbproject/build-impl.xml.script.CRC32=69f2059c
+nbproject/build-impl.xml.stylesheet.CRC32=bc42a706@1.3.0
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/nbproject/project.properties Mon Jan 11 23:11:31 2010 +0100
@@ -0,0 +1,77 @@
+application.title=Isabelle-jEdit
+application.vendor=makarius
+application.args=-noserver -nobackground
+build.classes.dir=${build.dir}/classes
+build.classes.excludes=**/*.java,**/*.form,**/*.scala
+# This directory is removed when the project is cleaned:
+build.dir=build
+build.generated.dir=${build.dir}/generated
+# Only compile against the classpath explicitly listed here:
+build.sysclasspath=ignore
+build.test.classes.dir=${build.dir}/test/classes
+build.test.results.dir=${build.dir}/test/results
+debug.classpath=\
+ ${run.classpath}
+debug.test.classpath=\
+ ${run.test.classpath}
+# This directory is removed when the project is cleaned:
+dist.dir=dist
+# dist can be used as jEdits settings-directory;
+# jEdit searches for plugins in the 'jars' subdirectory
+# must include something like this to private.properties:
+# application.args=-noserver -nobackground -settings=/absolute/path/to/project/dist
+#
+dist.jar=${dist.dir}/jars/Isabelle-jEdit.jar
+dist.javadoc.dir=${dist.dir}/javadoc
+excludes=
+file.reference.isabelle-jedit-src=src
+file.reference.jedit.jar=/home/makarius/lib/jedit/current/jedit.jar
+includes=**
+jar.compress=false
+java.platform.active=java_default_platform
+javac.classpath=\
+ ${reference.jEdit.build}:\
+ ${libs.Isabelle-Pure.classpath}:\
+ ${libs.Cobra-Renderer.classpath}:\
+ ${libs.Rhino-JavaScript.classpath}:\
+ ${libs.ErrorList.classpath}:\
+ ${libs.Hyperlinks.classpath}:\
+ ${libs.SideKick.classpath}:\
+ ${libs.Console.classpath}:\
+ ${libs.Scala-compiler.classpath}
+# Space-separated list of extra javac options
+javac.compilerargs=
+javac.deprecation=false
+javac.source=1.5
+javac.target=1.5
+javac.test.classpath=\
+ ${javac.classpath}:\
+ ${build.classes.dir}:\
+ ${libs.junit.classpath}:\
+ ${libs.junit_4.classpath}
+javadoc.additionalparam=
+javadoc.author=false
+javadoc.encoding=${source.encoding}
+javadoc.noindex=false
+javadoc.nonavbar=false
+javadoc.notree=false
+javadoc.private=false
+javadoc.splitindex=true
+javadoc.use=true
+javadoc.version=false
+javadoc.windowtitle=
+main.class=org.gjt.sp.jedit.jEdit
+manifest.file=manifest.mf
+meta.inf.dir=${src.dir}/META-INF
+platform.active=default_platform
+project.jEdit=contrib/jEdit
+reference.jEdit.build=${project.jEdit}/build/jEdit.jar
+run.classpath=\
+ ${javac.classpath}:\
+ ${build.classes.dir}
+run.jvmargs=-Xms128m -Xmx512m
+run.test.classpath=\
+ ${javac.test.classpath}:\
+ ${build.test.classes.dir}
+source.encoding=UTF-8
+src.dir=${file.reference.isabelle-jedit-src}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/nbproject/project.xml Mon Jan 11 23:11:31 2010 +0100
@@ -0,0 +1,24 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<project xmlns="http://www.netbeans.org/ns/project/1">
+ <type>org.netbeans.modules.scala.project</type>
+ <configuration>
+ <data xmlns="http://www.netbeans.org/ns/scala-project/1">
+ <name>Isabelle-jEdit</name>
+ <minimum-ant-version>1.6.5</minimum-ant-version>
+ <source-roots>
+ <root id="src.dir"/>
+ </source-roots>
+ <test-roots/>
+ </data>
+ <references xmlns="http://www.netbeans.org/ns/ant-project-references/1">
+ <reference>
+ <foreign-project>jEdit</foreign-project>
+ <artifact-type>jar</artifact-type>
+ <script>build-nb.xml</script>
+ <target>build</target>
+ <clean-target>clean</clean-target>
+ <id>build</id>
+ </reference>
+ </references>
+ </configuration>
+</project>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/plugin/Isabelle.props Mon Jan 11 23:11:31 2010 +0100
@@ -0,0 +1,48 @@
+## Isabelle plugin properties
+##
+##:encoding=ISO-8859-1:
+
+#identification
+plugin.isabelle.jedit.Plugin.name=Isabelle
+plugin.isabelle.jedit.Plugin.author=Johannes Hölzl, Fabian Immler, Makarius Wenzel
+plugin.isabelle.jedit.Plugin.version=0.0.1
+plugin.isabelle.jedit.Plugin.description=Isabelle/Isar asynchronous proof processing
+
+#system parameters
+plugin.isabelle.jedit.Plugin.activate=startup
+plugin.isabelle.jedit.Plugin.usePluginHome=false
+
+#dependencies
+plugin.isabelle.jedit.Plugin.depend.0=jdk 1.6
+plugin.isabelle.jedit.Plugin.depend.1=jedit 04.03.17.00
+plugin.isabelle.jedit.Plugin.depend.2=plugin errorlist.ErrorListPlugin 1.7
+plugin.isabelle.jedit.Plugin.depend.3=plugin sidekick.SideKickPlugin 0.7.6
+plugin.isabelle.jedit.Plugin.depend.4=plugin gatchan.jedit.hyperlinks.HyperlinksPlugin 1.0.1
+
+#options
+plugin.isabelle.jedit.Plugin.option-pane=isabelle
+options.isabelle.label=Isabelle
+options.isabelle.code=new isabelle.jedit.Isabelle_Options();
+options.isabelle.logic.title=Logic
+options.isabelle.font-size.title=Font Size
+options.isabelle.font-size=14
+options.isabelle.startup-timeout=10000
+
+#menu actions
+plugin.isabelle.jedit.Plugin.menu.label=Isabelle
+plugin.isabelle.jedit.Plugin.menu=isabelle.activate isabelle.show-output isabelle.show-protocol
+isabelle.activate.label=Activate current buffer
+isabelle.show-output.label=Show Output
+isabelle.show-protocol.label=Show Protocol
+
+#dockables
+isabelle-output.title=Output
+isabelle-protocol.title=Protocol
+
+#SideKick
+sidekick.parser.isabelle.label=Isabelle
+mode.isabelle.sidekick.parser=isabelle
+mode.ml.sidekick.parser=isabelle
+
+#Hyperlinks
+mode.isabelle.hyperlink.source=isabelle
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/plugin/actions.xml Mon Jan 11 23:11:31 2010 +0100
@@ -0,0 +1,23 @@
+<?xml version="1.0"?>
+<!DOCTYPE ACTIONS SYSTEM "actions.dtd">
+
+<ACTIONS>
+ <ACTION NAME="isabelle.activate">
+ <CODE>
+ isabelle.jedit.Isabelle.switch_active(view);
+ </CODE>
+ <IS_SELECTED>
+ return isabelle.jedit.Isabelle.is_active(view);
+ </IS_SELECTED>
+ </ACTION>
+ <ACTION NAME="isabelle.show-output">
+ <CODE>
+ wm.addDockableWindow("isabelle-output");
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.show-protocol">
+ <CODE>
+ wm.addDockableWindow("isabelle-protocol");
+ </CODE>
+ </ACTION>
+</ACTIONS>
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/plugin/dockables.xml Mon Jan 11 23:11:31 2010 +0100
@@ -0,0 +1,11 @@
+<?xml version="1.0"?>
+<!DOCTYPE DOCKABLES SYSTEM "dockables.dtd">
+
+<DOCKABLES>
+ <DOCKABLE NAME="isabelle-output" MOVABLE="TRUE">
+ new isabelle.jedit.Output_Dockable(view, position);
+ </DOCKABLE>
+ <DOCKABLE NAME="isabelle-protocol" MOVABLE="TRUE">
+ new isabelle.jedit.Protocol_Dockable(view, position);
+ </DOCKABLE>
+</DOCKABLES>
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/plugin/services.xml Mon Jan 11 23:11:31 2010 +0100
@@ -0,0 +1,17 @@
+<?xml version="1.0"?>
+<!DOCTYPE SERVICES SYSTEM "services.dtd">
+
+<SERVICES>
+ <SERVICE NAME="UTF-8-Isabelle" CLASS="org.gjt.sp.jedit.io.Encoding">
+ new isabelle.jedit.Isabelle_Encoding();
+ </SERVICE>
+ <SERVICE NAME="isabelle" CLASS="sidekick.SideKickParser">
+ new isabelle.jedit.Isabelle_Sidekick();
+ </SERVICE>
+ <SERVICE NAME="isabelle" CLASS="gatchan.jedit.hyperlinks.HyperlinkSource">
+ new isabelle.jedit.Isabelle_Hyperlinks();
+ </SERVICE>
+ <SERVICE CLASS="console.Shell" NAME="Scala">
+ new isabelle.jedit.Scala_Console();
+ </SERVICE>
+</SERVICES>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/Dummy.java Mon Jan 11 23:11:31 2010 +0100
@@ -0,0 +1,3 @@
+/* dummy class to make ant javadoc work */
+package isabelle;
+public class Dummy { }
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/document_model.scala Mon Jan 11 23:11:31 2010 +0100
@@ -0,0 +1,143 @@
+/*
+ * Document model connected to jEdit buffer
+ *
+ * @author Fabian Immler, TU Munich
+ * @author Makarius
+ */
+
+package isabelle.jedit
+
+
+import scala.actors.Actor, Actor._
+import scala.collection.mutable
+
+import org.gjt.sp.jedit.Buffer
+import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer}
+import org.gjt.sp.jedit.syntax.{ModeProvider, SyntaxStyle}
+
+
+object Document_Model
+{
+ /* document model of buffer */
+
+ private val key = "isabelle.document_model"
+
+ def init(session: Session, buffer: Buffer): Document_Model =
+ {
+ Swing_Thread.assert()
+ val model = new Document_Model(session, buffer)
+ buffer.setProperty(key, model)
+ model.activate()
+ model
+ }
+
+ def apply(buffer: Buffer): Option[Document_Model] =
+ {
+ Swing_Thread.assert()
+ buffer.getProperty(key) match {
+ case model: Document_Model => Some(model)
+ case _ => None
+ }
+ }
+
+ def exit(buffer: Buffer)
+ {
+ Swing_Thread.assert()
+ apply(buffer) match {
+ case None => error("No document model for buffer: " + buffer)
+ case Some(model) =>
+ model.deactivate()
+ buffer.unsetProperty(key)
+ }
+ }
+}
+
+class Document_Model(val session: Session, val buffer: Buffer)
+{
+ /* history */
+
+ private val document_0 = session.begin_document(buffer.getName)
+
+ @volatile private var history = // owned by Swing thread
+ new Change(document_0.id, None, Nil, Future.value(Nil, document_0))
+
+ def current_change(): Change = history
+ def recent_document(): Document = current_change().ancestors.find(_.is_assigned).get.join_document
+
+
+ /* transforming offsets */
+
+ private def changes_from(doc: Document): List[Text_Edit] =
+ {
+ Swing_Thread.assert()
+ (edits_buffer.toList /:
+ current_change.ancestors.takeWhile(_.id != doc.id))((edits, change) => change.edits ::: edits)
+ }
+
+ def from_current(doc: Document, offset: Int): Int =
+ (offset /: changes_from(doc).reverse) ((i, change) => change before i)
+
+ def to_current(doc: Document, offset: Int): Int =
+ (offset /: changes_from(doc)) ((i, change) => change after i)
+
+ def lines_of_command(doc: Document, cmd: Command): (Int, Int) =
+ {
+ val start = doc.command_start(cmd).get // FIXME total?
+ val stop = start + cmd.length
+ (buffer.getLineOfOffset(to_current(doc, start)),
+ buffer.getLineOfOffset(to_current(doc, stop)))
+ }
+
+
+ /* text edits */
+
+ private val edits_buffer = new mutable.ListBuffer[Text_Edit] // owned by Swing thread
+
+ private val edits_delay = Swing_Thread.delay_last(300) {
+ if (!edits_buffer.isEmpty) {
+ val new_change = current_change().edit(session, edits_buffer.toList)
+ edits_buffer.clear
+ history = new_change
+ new_change.result.map(_ => session.input(new_change))
+ }
+ }
+
+
+ /* buffer listener */
+
+ private val buffer_listener: BufferListener = new BufferAdapter
+ {
+ override def contentInserted(buffer: JEditBuffer,
+ start_line: Int, offset: Int, num_lines: Int, length: Int)
+ {
+ edits_buffer += new Text_Edit(true, offset, buffer.getText(offset, length))
+ edits_delay()
+ }
+
+ override def preContentRemoved(buffer: JEditBuffer,
+ start_line: Int, start: Int, num_lines: Int, removed_length: Int)
+ {
+ edits_buffer += new Text_Edit(false, start, buffer.getText(start, removed_length))
+ edits_delay()
+ }
+ }
+
+
+ /* activation */
+
+ def activate()
+ {
+ buffer.setTokenMarker(new Isabelle_Token_Marker(this))
+ buffer.addBufferListener(buffer_listener)
+ buffer.propertiesChanged()
+
+ edits_buffer += new Text_Edit(true, 0, buffer.getText(0, buffer.getLength))
+ edits_delay()
+ }
+
+ def deactivate()
+ {
+ buffer.setTokenMarker(buffer.getMode.getTokenMarker)
+ buffer.removeBufferListener(buffer_listener)
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/document_view.scala Mon Jan 11 23:11:31 2010 +0100
@@ -0,0 +1,301 @@
+/*
+ * Document view connected to jEdit text area
+ *
+ * @author Fabian Immler, TU Munich
+ * @author Makarius
+ */
+
+package isabelle.jedit
+
+
+import scala.actors.Actor._
+
+import java.awt.event.{MouseAdapter, MouseEvent}
+import java.awt.{BorderLayout, Graphics, Dimension, Color, Graphics2D}
+import javax.swing.{JPanel, ToolTipManager}
+import javax.swing.event.{CaretListener, CaretEvent}
+
+import org.gjt.sp.jedit.gui.RolloverButton
+import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
+
+
+object Document_View
+{
+ def choose_color(command: Command, doc: Document): Color =
+ {
+ doc.current_state(command).map(_.status) match {
+ case Some(Command.Status.UNPROCESSED) => new Color(255, 228, 225)
+ case Some(Command.Status.FINISHED) => new Color(234, 248, 255)
+ case Some(Command.Status.FAILED) => new Color(255, 193, 193)
+ case _ => Color.red
+ }
+ }
+
+
+ /* document view of text area */
+
+ private val key = new Object
+
+ def init(model: Document_Model, text_area: TextArea): Document_View =
+ {
+ Swing_Thread.assert()
+ val doc_view = new Document_View(model, text_area)
+ text_area.putClientProperty(key, doc_view)
+ doc_view.activate()
+ doc_view
+ }
+
+ def apply(text_area: TextArea): Option[Document_View] =
+ {
+ Swing_Thread.assert()
+ text_area.getClientProperty(key) match {
+ case doc_view: Document_View => Some(doc_view)
+ case _ => None
+ }
+ }
+
+ def exit(text_area: TextArea)
+ {
+ Swing_Thread.assert()
+ apply(text_area) match {
+ case None => error("No document view for text area: " + text_area)
+ case Some(doc_view) =>
+ doc_view.deactivate()
+ text_area.putClientProperty(key, null)
+ }
+ }
+}
+
+
+class Document_View(model: Document_Model, text_area: TextArea)
+{
+ private val session = model.session
+
+
+ /* visible document -- owned by Swing thread */
+
+ @volatile private var document = model.recent_document()
+
+
+ /* buffer of changed commands -- owned by Swing thread */
+
+ @volatile private var changed_commands: Set[Command] = Set()
+
+ private val changed_delay = Swing_Thread.delay_first(100) {
+ if (!changed_commands.isEmpty) {
+ document = model.recent_document()
+ for (cmd <- changed_commands if document.commands.contains(cmd)) { // FIXME cover doc states as well!!?
+ update_syntax(cmd)
+ invalidate_line(cmd)
+ overview.repaint()
+ }
+ changed_commands = Set()
+ }
+ }
+
+
+ /* command change actor */
+
+ private case object Exit
+
+ private val command_change_actor = actor {
+ loop {
+ react {
+ case command: Command => // FIXME rough filtering according to document family!?
+ Swing_Thread.now {
+ changed_commands += command
+ changed_delay()
+ }
+
+ case Exit => reply(()); exit()
+
+ case bad => System.err.println("command_change_actor: ignoring bad message " + bad)
+ }
+ }
+ }
+
+
+ /* text_area_extension */
+
+ private val text_area_extension = new TextAreaExtension
+ {
+ override def paintValidLine(gfx: Graphics2D,
+ screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
+ {
+ def from_current(pos: Int) = model.from_current(document, pos)
+ def to_current(pos: Int) = model.to_current(document, pos)
+ val metrics = text_area.getPainter.getFontMetrics
+ val saved_color = gfx.getColor
+ try {
+ for ((command, command_start) <-
+ document.command_range(from_current(start), from_current(end)))
+ {
+ val begin = start max to_current(command_start)
+ val finish = (end - 1) min to_current(command_start + command.length)
+ encolor(gfx, y, metrics.getHeight, begin, finish,
+ Document_View.choose_color(command, document), true)
+ }
+ }
+ finally { gfx.setColor(saved_color) }
+ }
+
+ override def getToolTipText(x: Int, y: Int): String =
+ {
+ val offset = model.from_current(document, text_area.xyToOffset(x, y))
+ document.command_at(offset) match {
+ case Some((command, command_start)) =>
+ document.current_state(command).get.type_at(offset - command_start).getOrElse(null)
+ case None => null
+ }
+ }
+ }
+
+
+ /* caret_listener */
+
+ private var _selected_command: Command = null
+ private def selected_command = _selected_command
+ private def selected_command_=(cmd: Command)
+ {
+ _selected_command = cmd
+ session.results.event(cmd)
+ }
+
+ private val caret_listener = new CaretListener
+ {
+ override def caretUpdate(e: CaretEvent)
+ {
+ document.command_at(e.getDot) match {
+ case Some((command, command_start)) if (selected_command != command) =>
+ selected_command = command
+ case _ =>
+ }
+ }
+ }
+
+
+ /* (re)painting */
+
+ private val update_delay = Swing_Thread.delay_first(500) { model.buffer.propertiesChanged() }
+
+ private def update_syntax(cmd: Command)
+ {
+ val (line1, line2) = model.lines_of_command(document, cmd)
+ if (line2 >= text_area.getFirstLine &&
+ line1 <= text_area.getFirstLine + text_area.getVisibleLines)
+ update_delay()
+ }
+
+ private def invalidate_line(cmd: Command) =
+ {
+ val (start, stop) = model.lines_of_command(document, cmd)
+ text_area.invalidateLineRange(start, stop)
+
+ if (selected_command == cmd)
+ session.results.event(cmd)
+ }
+
+ private def invalidate_all() =
+ text_area.invalidateLineRange(text_area.getFirstPhysicalLine,
+ text_area.getLastPhysicalLine)
+
+ private def encolor(gfx: Graphics2D,
+ y: Int, height: Int, begin: Int, finish: Int, color: Color, fill: Boolean)
+ {
+ val start = text_area.offsetToXY(begin)
+ val stop =
+ if (finish < model.buffer.getLength) text_area.offsetToXY(finish)
+ else {
+ val p = text_area.offsetToXY(finish - 1)
+ val metrics = text_area.getPainter.getFontMetrics
+ p.x = p.x + (metrics.charWidth(' ') max metrics.getMaxAdvance)
+ p
+ }
+
+ if (start != null && stop != null) {
+ gfx.setColor(color)
+ if (fill) gfx.fillRect(start.x, y, stop.x - start.x, height)
+ else gfx.drawRect(start.x, y, stop.x - start.x, height)
+ }
+ }
+
+
+ /* overview of command status left of scrollbar */
+
+ private val overview = new JPanel(new BorderLayout)
+ {
+ private val WIDTH = 10
+ private val HEIGHT = 2
+
+ setPreferredSize(new Dimension(WIDTH, 0))
+
+ setRequestFocusEnabled(false)
+
+ addMouseListener(new MouseAdapter {
+ override def mousePressed(event: MouseEvent) {
+ val line = y_to_line(event.getY)
+ if (line >= 0 && line < text_area.getLineCount)
+ text_area.setCaretPosition(text_area.getLineStartOffset(line))
+ }
+ })
+
+ override def addNotify() {
+ super.addNotify()
+ ToolTipManager.sharedInstance.registerComponent(this)
+ }
+
+ override def removeNotify() {
+ ToolTipManager.sharedInstance.unregisterComponent(this)
+ super.removeNotify
+ }
+
+ override def getToolTipText(event: MouseEvent): String =
+ {
+ val line = y_to_line(event.getY())
+ if (line >= 0 && line < text_area.getLineCount) "<html><b>TODO:</b><br>Tooltip</html>"
+ else ""
+ }
+
+ override def paintComponent(gfx: Graphics)
+ {
+ super.paintComponent(gfx)
+ val buffer = model.buffer
+
+ for ((command, start) <- document.command_range(0)) {
+ val line1 = buffer.getLineOfOffset(model.to_current(document, start))
+ val line2 = buffer.getLineOfOffset(model.to_current(document, start + command.length)) + 1
+ val y = line_to_y(line1)
+ val height = HEIGHT * (line2 - line1)
+ gfx.setColor(Document_View.choose_color(command, document))
+ gfx.fillRect(0, y, getWidth - 1, height)
+ }
+ }
+
+ private def line_to_y(line: Int): Int =
+ (line * getHeight) / (text_area.getBuffer.getLineCount max text_area.getVisibleLines)
+
+ private def y_to_line(y: Int): Int =
+ (y * (text_area.getBuffer.getLineCount max text_area.getVisibleLines)) / getHeight
+ }
+
+
+ /* activation */
+
+ private def activate()
+ {
+ text_area.getPainter.
+ addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension)
+ text_area.addCaretListener(caret_listener)
+ text_area.addLeftOfScrollBar(overview)
+ session.command_change += command_change_actor
+ }
+
+ private def deactivate()
+ {
+ session.command_change -= command_change_actor
+ command_change_actor !? Exit
+ text_area.removeLeftOfScrollBar(overview)
+ text_area.removeCaretListener(caret_listener)
+ text_area.getPainter.removeExtension(text_area_extension)
+ }
+}
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/html_panel.scala Mon Jan 11 23:11:31 2010 +0100
@@ -0,0 +1,140 @@
+/*
+ * HTML panel based on Lobo/Cobra
+ *
+ * @author Makarius
+ */
+
+package isabelle.jedit
+
+
+import java.io.StringReader
+import java.awt.{BorderLayout, Dimension}
+import java.awt.event.MouseEvent
+
+import javax.swing.{JButton, JPanel, JScrollPane}
+import java.util.logging.{Logger, Level}
+
+import org.w3c.dom.html2.HTMLElement
+
+import org.lobobrowser.html.parser.{DocumentBuilderImpl, InputSourceImpl}
+import org.lobobrowser.html.gui.HtmlPanel
+import org.lobobrowser.html.domimpl.{HTMLDocumentImpl, HTMLStyleElementImpl, NodeImpl}
+import org.lobobrowser.html.test.{SimpleHtmlRendererContext, SimpleUserAgentContext}
+
+import scala.io.Source
+import scala.actors.Actor._
+
+
+object HTML_Panel
+{
+ sealed abstract class Event { val element: HTMLElement; val mouse: MouseEvent }
+ case class Context_Menu(val element: HTMLElement, mouse: MouseEvent) extends Event
+ case class Mouse_Click(val element: HTMLElement, mouse: MouseEvent) extends Event
+ case class Double_Click(val element: HTMLElement, mouse: MouseEvent) extends Event
+ case class Mouse_Over(val element: HTMLElement, mouse: MouseEvent) extends Event
+ case class Mouse_Out(val element: HTMLElement, mouse: MouseEvent) extends Event
+}
+
+
+class HTML_Panel(
+ sys: Isabelle_System,
+ initial_font_size: Int,
+ handler: PartialFunction[HTML_Panel.Event, Unit]) extends HtmlPanel
+{
+ // global logging
+ Logger.getLogger("org.lobobrowser").setLevel(Level.WARNING)
+
+
+ /* document template */
+
+ private def try_file(name: String): String =
+ {
+ val file = sys.platform_file(name)
+ if (file.isFile) Source.fromFile(file).mkString else ""
+ }
+
+ private def template(font_size: Int): String =
+ """<?xml version="1.0" encoding="utf-8"?>
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
+ "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml">
+<head>
+<style media="all" type="text/css">
+""" +
+ try_file("$ISABELLE_HOME/lib/html/isabelle.css") + "\n" +
+ try_file("$ISABELLE_HOME_USER/etc/isabelle.css") + "\n" +
+ "body { font-family: " + sys.font_family + "; font-size: " + font_size + "px }" +
+"""
+</style>
+</head>
+<body/>
+</html>
+"""
+
+
+ /* actor with local state */
+
+ private val ucontext = new SimpleUserAgentContext
+
+ private val rcontext = new SimpleHtmlRendererContext(this, ucontext)
+ {
+ private def handle(event: HTML_Panel.Event): Boolean =
+ if (handler != null && handler.isDefinedAt(event)) { handler(event); true }
+ else false
+
+ override def onContextMenu(elem: HTMLElement, event: MouseEvent): Boolean =
+ handle(HTML_Panel.Context_Menu(elem, event))
+ override def onMouseClick(elem: HTMLElement, event: MouseEvent): Boolean =
+ handle(HTML_Panel.Mouse_Click(elem, event))
+ override def onDoubleClick(elem: HTMLElement, event: MouseEvent): Boolean =
+ handle(HTML_Panel.Double_Click(elem, event))
+ override def onMouseOver(elem: HTMLElement, event: MouseEvent)
+ { handle(HTML_Panel.Mouse_Over(elem, event)) }
+ override def onMouseOut(elem: HTMLElement, event: MouseEvent)
+ { handle(HTML_Panel.Mouse_Out(elem, event)) }
+ }
+
+ private val builder = new DocumentBuilderImpl(ucontext, rcontext)
+
+ private case class Init(font_size: Int)
+ private case class Render(body: List[XML.Tree])
+
+ private val main_actor = actor {
+ // crude double buffering
+ var doc1: org.w3c.dom.Document = null
+ var doc2: org.w3c.dom.Document = null
+
+ loop {
+ react {
+ case Init(font_size) =>
+ val src = template(font_size)
+ def parse() =
+ builder.parse(new InputSourceImpl(new StringReader(src), "http://localhost"))
+ doc1 = parse()
+ doc2 = parse()
+ Swing_Thread.now { setDocument(doc1, rcontext) }
+
+ case Render(body) =>
+ val doc = doc2
+ val node =
+ XML.document_node(doc,
+ XML.elem(HTML.BODY, body.map((t: XML.Tree) => XML.elem(HTML.PRE, HTML.spans(t)))))
+ doc.removeChild(doc.getLastChild())
+ doc.appendChild(node)
+ doc2 = doc1
+ doc1 = doc
+ Swing_Thread.now { setDocument(doc1, rcontext) }
+
+ case bad => System.err.println("main_actor: ignoring bad message " + bad)
+ }
+ }
+ }
+
+ main_actor ! Init(initial_font_size)
+
+
+ /* main method wrappers */
+
+ def init(font_size: Int) { main_actor ! Init(font_size) }
+ def render(body: List[XML.Tree]) { main_actor ! Render(body) }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/isabelle_encoding.scala Mon Jan 11 23:11:31 2010 +0100
@@ -0,0 +1,64 @@
+/*
+ * Isabelle encoding -- based on utf-8
+ *
+ * @author Makarius
+ */
+
+package isabelle.jedit
+
+
+import org.gjt.sp.jedit.io.Encoding
+import org.gjt.sp.jedit.buffer.JEditBuffer
+
+import java.nio.charset.{Charset, CharsetDecoder, CodingErrorAction}
+import java.io.{InputStream, OutputStream, Reader, Writer, InputStreamReader, OutputStreamWriter,
+ CharArrayReader, ByteArrayOutputStream}
+
+import scala.io.{Source, BufferedSource}
+
+
+object Isabelle_Encoding
+{
+ val NAME = "UTF-8-Isabelle"
+
+ def is_active(buffer: JEditBuffer): Boolean =
+ buffer.getStringProperty(JEditBuffer.ENCODING).asInstanceOf[String] == NAME
+}
+
+class Isabelle_Encoding extends Encoding
+{
+ private val charset = Charset.forName(Standard_System.charset)
+ private val BUFSIZE = 32768
+
+ private def text_reader(in: InputStream, decoder: CharsetDecoder): Reader =
+ {
+ def source(): Source =
+ BufferedSource.fromInputStream(in, decoder, BUFSIZE, { () => source() })
+ new CharArrayReader(Isabelle.system.symbols.decode(source.mkString).toArray)
+ }
+
+ override def getTextReader(in: InputStream): Reader =
+ text_reader(in, charset.newDecoder())
+
+ override def getPermissiveTextReader(in: InputStream): Reader =
+ {
+ val decoder = charset.newDecoder()
+ decoder.onMalformedInput(CodingErrorAction.REPLACE)
+ decoder.onUnmappableCharacter(CodingErrorAction.REPLACE)
+ text_reader(in, decoder)
+ }
+
+ override def getTextWriter(out: OutputStream): Writer =
+ {
+ val buffer = new ByteArrayOutputStream(BUFSIZE) {
+ override def flush()
+ {
+ val text = Isabelle.system.symbols.encode(toString(Standard_System.charset))
+ out.write(text.getBytes(Standard_System.charset))
+ out.flush()
+ }
+ override def close() { out.close() }
+ }
+ new OutputStreamWriter(buffer, charset.newEncoder())
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Mon Jan 11 23:11:31 2010 +0100
@@ -0,0 +1,75 @@
+/*
+ * Hyperlink setup for Isabelle proof documents
+ *
+ * @author Fabian Immler, TU Munich
+ */
+
+package isabelle.jedit
+
+
+import java.io.File
+
+import gatchan.jedit.hyperlinks.{Hyperlink, HyperlinkSource, AbstractHyperlink}
+
+import org.gjt.sp.jedit.{View, jEdit, Buffer, TextUtilities}
+
+
+private class Internal_Hyperlink(start: Int, end: Int, line: Int, ref_offset: Int)
+ extends AbstractHyperlink(start, end, line, "")
+{
+ override def click(view: View) {
+ view.getTextArea.moveCaretPosition(ref_offset)
+ }
+}
+
+class External_Hyperlink(start: Int, end: Int, line: Int, ref_file: String, ref_line: Int)
+ extends AbstractHyperlink(start, end, line, "")
+{
+ override def click(view: View) = {
+ Isabelle.system.source_file(ref_file) match {
+ case None => System.err.println("Could not find source file " + ref_file) // FIXME ??
+ case Some(file) =>
+ jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + ref_line))
+ }
+ }
+}
+
+class Isabelle_Hyperlinks extends HyperlinkSource
+{
+ def getHyperlink(buffer: Buffer, original_offset: Int): Hyperlink =
+ {
+ Document_Model(buffer) match {
+ case Some(model) =>
+ val document = model.recent_document()
+ val offset = model.from_current(document, original_offset)
+ document.command_at(offset) match {
+ case Some((command, command_start)) =>
+ document.current_state(command).get.ref_at(offset - command_start) match {
+ case Some(ref) =>
+ val begin = model.to_current(document, command_start + ref.start)
+ val line = buffer.getLineOfOffset(begin)
+ val end = model.to_current(document, command_start + ref.stop)
+ ref.info match {
+ case Command.RefInfo(Some(ref_file), Some(ref_line), _, _) =>
+ new External_Hyperlink(begin, end, line, ref_file, ref_line)
+ case Command.RefInfo(_, _, Some(id), Some(offset)) =>
+ Isabelle.session.lookup_entity(id) match {
+ case Some(ref_cmd: Command) =>
+ document.command_start(ref_cmd) match {
+ case Some(ref_cmd_start) =>
+ new Internal_Hyperlink(begin, end, line,
+ model.to_current(document, ref_cmd_start + offset - 1))
+ case None => null // FIXME external ref
+ }
+ case _ => null
+ }
+ case _ => null
+ }
+ case None => null
+ }
+ case None => null
+ }
+ case None => null
+ }
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/isabelle_options.scala Mon Jan 11 23:11:31 2010 +0100
@@ -0,0 +1,53 @@
+/*
+ * Editor pane for plugin options
+ *
+ * @author Johannes Hölzl, TU Munich
+ */
+
+package isabelle.jedit
+
+
+import javax.swing.{JComboBox, JSpinner}
+
+import org.gjt.sp.jedit.AbstractOptionPane
+
+
+class Isabelle_Options extends AbstractOptionPane("isabelle")
+{
+ private val logic_name = new JComboBox()
+ private val font_size = new JSpinner()
+
+ private class List_Item(val name: String, val descr: String) {
+ def this(name: String) = this(name, name)
+ override def toString = descr
+ }
+
+ override def _init()
+ {
+ val logic = Isabelle.Property("logic")
+ addComponent(Isabelle.Property("logic.title"), {
+ logic_name.addItem(new List_Item("", "default (" + Isabelle.default_logic() + ")"))
+ for (name <- Isabelle.system.find_logics()) {
+ val item = new List_Item(name)
+ logic_name.addItem(item)
+ if (name == logic)
+ logic_name.setSelectedItem(item)
+ }
+ logic_name
+ })
+
+ addComponent(Isabelle.Property("font-size.title"), {
+ font_size.setValue(Isabelle.Int_Property("font-size"))
+ font_size
+ })
+ }
+
+ override def _save()
+ {
+ val logic = logic_name.getSelectedItem.asInstanceOf[List_Item].name
+ Isabelle.Property("logic") = logic
+
+ val size = font_size.getValue().asInstanceOf[Int]
+ Isabelle.Int_Property("font-size") = size
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Mon Jan 11 23:11:31 2010 +0100
@@ -0,0 +1,98 @@
+/*
+ * SideKick parser for Isabelle proof documents
+ *
+ * @author Fabian Immler, TU Munich
+ * @author Makarius
+ */
+
+package isabelle.jedit
+
+
+import scala.collection.Set
+import scala.collection.immutable.TreeSet
+
+import javax.swing.tree.DefaultMutableTreeNode
+import javax.swing.text.Position
+import javax.swing.Icon
+
+import org.gjt.sp.jedit.{Buffer, EditPane, TextUtilities, View}
+import errorlist.DefaultErrorSource
+import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, IAsset}
+
+
+class Isabelle_Sidekick extends SideKickParser("isabelle")
+{
+ /* parsing */
+
+ @volatile private var stopped = false
+ override def stop() = { stopped = true }
+
+ def parse(buffer: Buffer, error_source: DefaultErrorSource): SideKickParsedData =
+ {
+ implicit def int_to_pos(offset: Int): Position =
+ new Position { def getOffset = offset; override def toString = offset.toString }
+
+ stopped = false
+
+ // FIXME lock buffer !??
+ val data = new SideKickParsedData(buffer.getName)
+ val root = data.root
+ data.getAsset(root).setEnd(buffer.getLength)
+
+ Swing_Thread.now { Document_Model(buffer) } match {
+ case Some(model) =>
+ val document = model.recent_document()
+ for ((command, command_start) <- document.command_range(0) if !stopped) {
+ root.add(document.current_state(command).get.markup_root.swing_tree((node: Markup_Node) =>
+ {
+ val content = command.source(node.start, node.stop)
+ val id = command.id
+
+ new DefaultMutableTreeNode(new IAsset {
+ override def getIcon: Icon = null
+ override def getShortString: String = content
+ override def getLongString: String = node.info.toString
+ override def getName: String = id
+ override def setName(name: String) = ()
+ override def setStart(start: Position) = ()
+ override def getStart: Position = command_start + node.start
+ override def setEnd(end: Position) = ()
+ override def getEnd: Position = command_start + node.stop
+ override def toString = id + ": " + content + "[" + getStart + " - " + getEnd + "]"
+ })
+ }))
+ }
+ if (stopped) root.add(new DefaultMutableTreeNode("<parser stopped>"))
+ case None => root.add(new DefaultMutableTreeNode("<buffer inactive>"))
+ }
+ data
+ }
+
+
+ /* completion */
+
+ override def supportsCompletion = true
+ override def canCompleteAnywhere = true
+
+ override def complete(pane: EditPane, caret: Int): SideKickCompletion =
+ {
+ val buffer = pane.getBuffer
+
+ val line = buffer.getLineOfOffset(caret)
+ val start = buffer.getLineStartOffset(line)
+ val text = buffer.getSegment(start, caret - start)
+
+ val completion = Isabelle.session.current_syntax.completion
+
+ completion.complete(text) match {
+ case None => null
+ case Some((word, cs)) =>
+ val ds =
+ if (Isabelle_Encoding.is_active(buffer))
+ cs.map(Isabelle.system.symbols.decode(_)).sort(_ < _)
+ else cs
+ new SideKickCompletion(pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { }
+ }
+ }
+
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala Mon Jan 11 23:11:31 2010 +0100
@@ -0,0 +1,145 @@
+/*
+ * include isabelle's command- and keyword-declarations
+ * live in jEdits syntax-highlighting
+ *
+ * @author Fabian Immler, TU Munich
+ */
+
+package isabelle.jedit
+
+
+import isabelle.Markup
+
+import org.gjt.sp.jedit.buffer.JEditBuffer
+import org.gjt.sp.jedit.syntax.{Token, TokenMarker, TokenHandler, SyntaxStyle, ParserRuleSet}
+
+import java.awt.Color
+import java.awt.Font
+import javax.swing.text.Segment;
+
+
+object Isabelle_Token_Marker
+{
+ /* line context */
+
+ private val rule_set = new ParserRuleSet("isabelle", "MAIN")
+ private class LineContext(val line: Int, prev: LineContext)
+ extends TokenMarker.LineContext(rule_set, prev)
+
+
+ /* mapping to jEdit token types */
+ // TODO: as properties or CSS style sheet
+
+ private val choose_byte: Map[String, Byte] =
+ {
+ import Token._
+ Map[String, Byte](
+ // logical entities
+ Markup.TCLASS -> LABEL,
+ Markup.TYCON -> LABEL,
+ Markup.FIXED_DECL -> LABEL,
+ Markup.FIXED -> LABEL,
+ Markup.CONST_DECL -> LABEL,
+ Markup.CONST -> LABEL,
+ Markup.FACT_DECL -> LABEL,
+ Markup.FACT -> LABEL,
+ Markup.DYNAMIC_FACT -> LABEL,
+ Markup.LOCAL_FACT_DECL -> LABEL,
+ Markup.LOCAL_FACT -> LABEL,
+ // inner syntax
+ Markup.TFREE -> LITERAL2,
+ Markup.FREE -> LITERAL2,
+ Markup.TVAR -> LITERAL3,
+ Markup.SKOLEM -> LITERAL3,
+ Markup.BOUND -> LITERAL3,
+ Markup.VAR -> LITERAL3,
+ Markup.NUM -> DIGIT,
+ Markup.FLOAT -> DIGIT,
+ Markup.XNUM -> DIGIT,
+ Markup.XSTR -> LITERAL4,
+ Markup.LITERAL -> LITERAL4,
+ Markup.INNER_COMMENT -> COMMENT1,
+ Markup.SORT -> FUNCTION,
+ Markup.TYP -> FUNCTION,
+ Markup.TERM -> FUNCTION,
+ Markup.PROP -> FUNCTION,
+ Markup.ATTRIBUTE -> FUNCTION,
+ Markup.METHOD -> FUNCTION,
+ // ML syntax
+ Markup.ML_KEYWORD -> KEYWORD2,
+ Markup.ML_IDENT -> NULL,
+ Markup.ML_TVAR -> LITERAL3,
+ Markup.ML_NUMERAL -> DIGIT,
+ Markup.ML_CHAR -> LITERAL1,
+ Markup.ML_STRING -> LITERAL1,
+ Markup.ML_COMMENT -> COMMENT1,
+ Markup.ML_MALFORMED -> INVALID,
+ // embedded source text
+ Markup.ML_SOURCE -> COMMENT4,
+ Markup.DOC_SOURCE -> COMMENT4,
+ Markup.ANTIQ -> COMMENT4,
+ Markup.ML_ANTIQ -> COMMENT4,
+ Markup.DOC_ANTIQ -> COMMENT4,
+ // outer syntax
+ Markup.IDENT -> NULL,
+ Markup.COMMAND -> OPERATOR,
+ Markup.KEYWORD -> KEYWORD4,
+ Markup.VERBATIM -> COMMENT3,
+ Markup.COMMENT -> COMMENT1,
+ Markup.CONTROL -> COMMENT3,
+ Markup.MALFORMED -> INVALID,
+ Markup.STRING -> LITERAL3,
+ Markup.ALTSTRING -> LITERAL1
+ ).withDefaultValue(NULL)
+ }
+
+ def choose_color(kind: String, styles: Array[SyntaxStyle]): Color =
+ styles(choose_byte(kind)).getForegroundColor
+}
+
+
+class Isabelle_Token_Marker(model: Document_Model) extends TokenMarker
+{
+ override def markTokens(prev: TokenMarker.LineContext,
+ handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext =
+ {
+ val previous = prev.asInstanceOf[Isabelle_Token_Marker.LineContext]
+ val line = if (prev == null) 0 else previous.line + 1
+ val context = new Isabelle_Token_Marker.LineContext(line, previous)
+ val start = model.buffer.getLineStartOffset(line)
+ val stop = start + line_segment.count
+
+ val document = model.recent_document()
+ def to: Int => Int = model.to_current(document, _)
+ def from: Int => Int = model.from_current(document, _)
+
+ var next_x = start
+ for {
+ (command, command_start) <- document.command_range(from(start), from(stop))
+ markup <- document.current_state(command).get.highlight.flatten
+ val abs_start = to(command_start + markup.start)
+ val abs_stop = to(command_start + markup.stop)
+ if (abs_stop > start)
+ if (abs_start < stop)
+ val byte = Isabelle_Token_Marker.choose_byte(markup.info.toString)
+ val token_start = (abs_start - start) max 0
+ val token_length =
+ (abs_stop - abs_start) -
+ ((start - abs_start) max 0) -
+ ((abs_stop - stop) max 0)
+ }
+ {
+ if (start + token_start > next_x)
+ handler.handleToken(line_segment, 1,
+ next_x - start, start + token_start - next_x, context)
+ handler.handleToken(line_segment, byte, token_start, token_length, context)
+ next_x = start + token_start + token_length
+ }
+ if (next_x < stop)
+ handler.handleToken(line_segment, 1, next_x - start, stop - next_x, context)
+
+ handler.handleToken(line_segment, Token.END, line_segment.count, 0, context)
+ handler.setLineContext(context)
+ context
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala Mon Jan 11 23:11:31 2010 +0100
@@ -0,0 +1,64 @@
+/*
+ * Dockable window with result message output
+ *
+ * @author Makarius
+ */
+
+package isabelle.jedit
+
+
+import scala.actors.Actor._
+
+import javax.swing.JPanel
+import java.awt.{BorderLayout, Dimension}
+
+import org.gjt.sp.jedit.View
+import org.gjt.sp.jedit.gui.DockableWindowManager
+
+
+
+class Output_Dockable(view: View, position: String) extends JPanel(new BorderLayout)
+{
+ if (position == DockableWindowManager.FLOATING)
+ setPreferredSize(new Dimension(500, 250))
+
+ private val html_panel =
+ new HTML_Panel(Isabelle.system, Isabelle.Int_Property("font-size"), null)
+ add(html_panel, BorderLayout.CENTER)
+
+
+ /* actor wiring */
+
+ private val output_actor = actor {
+ loop {
+ react {
+ case cmd: Command =>
+ Swing_Thread.now { Document_Model(view.getBuffer) } match {
+ case None =>
+ case Some(model) =>
+ val body = model.recent_document.current_state(cmd).map(_.results) getOrElse Nil
+ html_panel.render(body)
+ }
+
+ case Session.Global_Settings =>
+ html_panel.init(Isabelle.Int_Property("font-size"))
+
+ case bad => System.err.println("output_actor: ignoring bad message " + bad)
+ }
+ }
+ }
+
+ override def addNotify()
+ {
+ super.addNotify()
+ Isabelle.session.results += output_actor
+ Isabelle.session.global_settings += output_actor
+ }
+
+ override def removeNotify()
+ {
+ Isabelle.session.results -= output_actor
+ Isabelle.session.global_settings -= output_actor
+ super.removeNotify()
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/plugin.scala Mon Jan 11 23:11:31 2010 +0100
@@ -0,0 +1,195 @@
+/*
+ * Main Isabelle/jEdit plugin setup
+ *
+ * @author Johannes Hölzl, TU Munich
+ * @author Fabian Immler, TU Munich
+ * @author Makarius
+ */
+
+package isabelle.jedit
+
+
+import java.io.{FileInputStream, IOException}
+import java.awt.Font
+import javax.swing.JTextArea
+
+import scala.collection.mutable
+
+import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, EditPane, ServiceManager, View}
+import org.gjt.sp.jedit.buffer.JEditBuffer
+import org.gjt.sp.jedit.textarea.JEditTextArea
+import org.gjt.sp.jedit.msg.{EditPaneUpdate, PropertiesChanged}
+
+
+object Isabelle
+{
+ /* plugin instance */
+
+ var system: Isabelle_System = null
+ var session: Session = null
+
+
+ /* name */
+
+ val NAME = "Isabelle"
+
+
+ /* properties */
+
+ val OPTION_PREFIX = "options.isabelle."
+
+ object Property
+ {
+ def apply(name: String): String = jEdit.getProperty(OPTION_PREFIX + name)
+ def update(name: String, value: String) = jEdit.setProperty(OPTION_PREFIX + name, value)
+ }
+
+ object Boolean_Property
+ {
+ def apply(name: String): Boolean = jEdit.getBooleanProperty(OPTION_PREFIX + name)
+ def update(name: String, value: Boolean) = jEdit.setBooleanProperty(OPTION_PREFIX + name, value)
+ }
+
+ object Int_Property
+ {
+ def apply(name: String): Int = jEdit.getIntegerProperty(OPTION_PREFIX + name)
+ def update(name: String, value: Int) = jEdit.setIntegerProperty(OPTION_PREFIX + name, value)
+ }
+
+
+ /* settings */
+
+ def default_logic(): String =
+ {
+ val logic = system.getenv("JEDIT_LOGIC")
+ if (logic != "") logic
+ else system.getenv_strict("ISABELLE_LOGIC")
+ }
+
+ def isabelle_args(): List[String] =
+ {
+ val modes = system.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _)
+ val logic = {
+ val logic = Property("logic")
+ if (logic != null && logic != "") logic
+ else default_logic()
+ }
+ modes ++ List(logic)
+ }
+
+
+ /* main jEdit components */ // FIXME ownership!?
+
+ def jedit_buffers(): Iterator[Buffer] = Iterator.fromArray(jEdit.getBuffers())
+
+ def jedit_views(): Iterator[View] = Iterator.fromArray(jEdit.getViews())
+
+ def jedit_text_areas(view: View): Iterator[JEditTextArea] =
+ Iterator.fromArray(view.getEditPanes).map(_.getTextArea)
+
+ def jedit_text_areas(): Iterator[JEditTextArea] =
+ jedit_views().flatMap(jedit_text_areas(_))
+
+ def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] =
+ jedit_text_areas().filter(_.getBuffer == buffer)
+
+
+ /* manage prover */
+
+ private def prover_started(view: View): Boolean =
+ {
+ val timeout = Int_Property("startup-timeout") max 1000
+ session.start(timeout, Isabelle.isabelle_args()) match {
+ case Some(err) =>
+ val text = new JTextArea(err); text.setEditable(false)
+ Library.error_dialog(view, null, "Failed to start Isabelle process", text)
+ false
+ case None => true
+ }
+ }
+
+
+ /* activation */
+
+ def activate_buffer(view: View, buffer: Buffer)
+ {
+ if (prover_started(view)) {
+ val model = Document_Model.init(session, buffer)
+ for (text_area <- jedit_text_areas(buffer))
+ Document_View.init(model, text_area)
+ }
+ }
+
+ def deactivate_buffer(buffer: Buffer)
+ {
+ session.stop() // FIXME not yet
+
+ for (text_area <- jedit_text_areas(buffer))
+ Document_View.exit(text_area)
+ Document_Model.exit(buffer)
+ }
+
+ def switch_active(view: View) =
+ {
+ val buffer = view.getBuffer
+ if (Document_Model(buffer).isDefined) deactivate_buffer(buffer)
+ else activate_buffer(view, buffer)
+ }
+
+ def is_active(view: View): Boolean =
+ Document_Model(view.getBuffer).isDefined
+}
+
+
+class Plugin extends EBPlugin
+{
+ /* main plugin plumbing */
+
+ override def handleMessage(message: EBMessage)
+ {
+ message match {
+ case msg: EditPaneUpdate =>
+ val edit_pane = msg.getEditPane
+ val buffer = edit_pane.getBuffer
+ val text_area = edit_pane.getTextArea
+
+ def init_view()
+ {
+ Document_Model(buffer) match {
+ case Some(model) => Document_View.init(model, text_area)
+ case None =>
+ }
+ }
+ def exit_view()
+ {
+ if (Document_View(text_area).isDefined)
+ Document_View.exit(text_area)
+ }
+ msg.getWhat match {
+ case EditPaneUpdate.BUFFER_CHANGED => exit_view(); init_view()
+ case EditPaneUpdate.CREATED => init_view()
+ case EditPaneUpdate.DESTROYED => exit_view()
+ case _ =>
+ }
+
+ case msg: PropertiesChanged =>
+ Isabelle.session.global_settings.event(Session.Global_Settings)
+
+ case _ =>
+ }
+ }
+
+ override def start()
+ {
+ Isabelle.system = new Isabelle_System
+ Isabelle.system.install_fonts()
+ Isabelle.session = new Session(Isabelle.system) // FIXME dialog!?
+ }
+
+ override def stop()
+ {
+ Isabelle.session.stop() // FIXME dialog!?
+ Isabelle.session = null
+ Isabelle.system = null
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/protocol_dockable.scala Mon Jan 11 23:11:31 2010 +0100
@@ -0,0 +1,52 @@
+/*
+ * Dockable window for raw process output
+ *
+ * @author Makarius
+ */
+
+package isabelle.jedit
+
+
+import scala.actors.Actor._
+
+import java.awt.{Dimension, Graphics, BorderLayout}
+import javax.swing.{JPanel, JTextArea, JScrollPane}
+
+import org.gjt.sp.jedit.View
+import org.gjt.sp.jedit.gui.DockableWindowManager
+
+
+class Protocol_Dockable(view: View, position: String) extends JPanel(new BorderLayout)
+{
+ if (position == DockableWindowManager.FLOATING)
+ setPreferredSize(new Dimension(500, 250))
+
+ private val text_area = new JTextArea
+ add(new JScrollPane(text_area), BorderLayout.CENTER)
+
+
+ /* actor wiring */
+
+ private val raw_actor = actor {
+ loop {
+ react {
+ case result: Isabelle_Process.Result =>
+ Swing_Thread.now { text_area.append(result.toString + "\n") }
+
+ case bad => System.err.println("raw_actor: ignoring bad message " + bad)
+ }
+ }
+ }
+
+ override def addNotify()
+ {
+ super.addNotify()
+ Isabelle.session.raw_results += raw_actor
+ }
+
+ override def removeNotify()
+ {
+ Isabelle.session.raw_results -= raw_actor
+ super.removeNotify()
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/scala_console.scala Mon Jan 11 23:11:31 2010 +0100
@@ -0,0 +1,153 @@
+/*
+ * Scala instance of Console plugin
+ *
+ * @author Makarius
+ */
+
+package isabelle.jedit
+
+
+import console.{Console, ConsolePane, Shell, Output}
+
+import org.gjt.sp.jedit.{jEdit, JARClassLoader}
+import org.gjt.sp.jedit.MiscUtilities
+
+import java.io.{File, OutputStream, Writer, PrintWriter}
+
+import scala.tools.nsc.{Interpreter, GenericRunnerSettings, NewLinePrintWriter, ConsoleWriter}
+import scala.collection.mutable
+
+
+class Scala_Console extends Shell("Scala")
+{
+ /* reconstructed jEdit/plugin classpath */
+
+ private def reconstruct_classpath(): String =
+ {
+ def find_jars(start: String): List[String] =
+ if (start != null)
+ Standard_System.find_files(new File(start),
+ entry => entry.isFile && entry.getName.endsWith(".jar")).map(_.getAbsolutePath)
+ else Nil
+ val path = find_jars(jEdit.getSettingsDirectory) ::: find_jars(jEdit.getJEditHome)
+ path.mkString(File.pathSeparator)
+ }
+
+
+ /* global state -- owned by Swing thread */
+
+ private var interpreters = Map[Console, Interpreter]()
+
+ private var global_console: Console = null
+ private var global_out: Output = null
+ private var global_err: Output = null
+
+ private val console_stream = new OutputStream
+ {
+ val buf = new StringBuilder
+ override def flush()
+ {
+ val str = Standard_System.decode_permissive_utf8(buf.toString)
+ buf.clear
+ if (global_out == null) System.out.print(str)
+ else Swing_Thread.now { global_out.writeAttrs(null, str) }
+ }
+ override def close() { flush () }
+ def write(byte: Int) { buf.append(byte.toChar) }
+ }
+
+ private val console_writer = new Writer
+ {
+ def flush() {}
+ def close() {}
+
+ def write(cbuf: Array[Char], off: Int, len: Int)
+ {
+ if (len > 0) write(new String(cbuf.subArray(off, off + len)))
+ }
+
+ override def write(str: String)
+ {
+ if (global_out == null) System.out.println(str)
+ else global_out.print(null, str)
+ }
+ }
+
+ private def with_console[A](console: Console, out: Output, err: Output)(e: => A): A =
+ {
+ global_console = console
+ global_out = out
+ global_err = if (err == null) out else err
+ val res = Exn.capture { scala.Console.withOut(console_stream)(e) }
+ console_stream.flush
+ global_console = null
+ global_out = null
+ global_err = null
+ Exn.release(res)
+ }
+
+ private def report_error(str: String)
+ {
+ if (global_console == null || global_err == null) System.err.println(str)
+ else Swing_Thread.now { global_err.print(global_console.getErrorColor, str) }
+ }
+
+
+ /* jEdit console methods */
+
+ override def openConsole(console: Console)
+ {
+ val settings = new GenericRunnerSettings(report_error)
+ settings.classpath.value = reconstruct_classpath()
+
+ val interp = new Interpreter(settings, new PrintWriter(console_writer, true))
+ {
+ override def parentClassLoader = new JARClassLoader
+ }
+ interp.setContextClassLoader
+ interp.bind("view", "org.gjt.sp.jedit.View", console.getView)
+ interp.bind("console", "console.Console", console)
+ interp.interpret("import isabelle.jedit.Isabelle")
+
+ interpreters += (console -> interp)
+ }
+
+ override def closeConsole(console: Console)
+ {
+ interpreters -= console
+ }
+
+ override def printInfoMessage(out: Output)
+ {
+ out.print(null,
+ "This shell evaluates Isabelle/Scala expressions.\n\n" +
+ "The following special toplevel bindings are provided:\n" +
+ " view -- current jEdit/Swing view (e.g. view.getBuffer, view.getTextArea)\n" +
+ " console -- jEdit Console plugin instance\n" +
+ " Isabelle -- Isabelle plugin instance (e.g. Isabelle.system, Isabelle.session)\n")
+ }
+
+ override def printPrompt(console: Console, out: Output)
+ {
+ out.writeAttrs(ConsolePane.colorAttributes(console.getInfoColor), "scala>")
+ out.writeAttrs(ConsolePane.colorAttributes(console.getPlainColor), " ")
+ }
+
+ override def execute(console: Console, input: String, out: Output, err: Output, command: String)
+ {
+ val interp = interpreters(console)
+ with_console(console, out, err) { interp.interpret(command) }
+ if (err != null) err.commandDone()
+ out.commandDone()
+ }
+
+ override def stop(console: Console)
+ {
+ closeConsole(console)
+ console.clear
+ openConsole(console)
+ val out = console.getOutput
+ out.commandDone
+ printPrompt(console, out)
+ }
+}