1.1 --- a/.hgignore Mon Jan 11 16:45:02 2010 +0100
1.2 +++ b/.hgignore Mon Jan 11 23:11:31 2010 +0100
1.3 @@ -24,4 +24,7 @@
1.4 ^doc-src/.*\.rao
1.5 ^doc-src/.*\.toc
1.6
1.7 -
1.8 +^src/Tools/jEdit/nbproject/private/
1.9 +^src/Tools/jEdit/build/
1.10 +^src/Tools/jEdit/dist/
1.11 +^src/Tools/jEdit/contrib/
2.1 --- a/src/Pure/General/exn.scala Mon Jan 11 16:45:02 2010 +0100
2.2 +++ b/src/Pure/General/exn.scala Mon Jan 11 23:11:31 2010 +0100
2.3 @@ -1,7 +1,7 @@
2.4 /* Title: Pure/General/exn.scala
2.5 Author: Makarius
2.6
2.7 -Extra support for exceptions.
2.8 +Extra support for exceptions (arbitrary throwables).
2.9 */
2.10
2.11 package isabelle
2.12 @@ -13,11 +13,11 @@
2.13
2.14 sealed abstract class Result[A]
2.15 case class Res[A](val result: A) extends Result[A]
2.16 - case class Exn[A](val exn: Exception) extends Result[A]
2.17 + case class Exn[A](val exn: Throwable) extends Result[A]
2.18
2.19 def capture[A](e: => A): Result[A] =
2.20 try { Res(e) }
2.21 - catch { case exn: RuntimeException => Exn[A](exn) } // FIXME *all* exceptions (!?), cf. ML version
2.22 + catch { case exn: Throwable => Exn[A](exn) }
2.23
2.24 def release[A](result: Result[A]): A =
2.25 result match {
3.1 --- a/src/Pure/General/scan.scala Mon Jan 11 16:45:02 2010 +0100
3.2 +++ b/src/Pure/General/scan.scala Mon Jan 11 23:11:31 2010 +0100
3.3 @@ -179,7 +179,7 @@
3.4 private def quoted(quote: String): Parser[String] =
3.5 {
3.6 quote ~
3.7 - rep(many1(sym => sym != quote && sym != "\\" && Symbol.is_closed(sym)) |
3.8 + rep(many1(sym => sym != quote && sym != "\\" && Symbol.is_wellformed(sym)) |
3.9 "\\" + quote | "\\\\" |
3.10 (("""\\\d\d\d""".r) ^? { case x if x.substring(1, 4).toInt <= 255 => x })) ~
3.11 quote ^^ { case x ~ ys ~ z => x + ys.mkString + z }
3.12 @@ -191,7 +191,7 @@
3.13 val body = source.substring(1, source.length - 1)
3.14 if (body.exists(_ == '\\')) {
3.15 val content =
3.16 - rep(many1(sym => sym != quote && sym != "\\" && Symbol.is_closed(sym)) |
3.17 + rep(many1(sym => sym != quote && sym != "\\" && Symbol.is_wellformed(sym)) |
3.18 "\\" ~> (quote | "\\" | """\d\d\d""".r ^^ { case x => x.toInt.toChar.toString }))
3.19 parseAll(content ^^ (_.mkString), body).get
3.20 }
3.21 @@ -203,7 +203,7 @@
3.22
3.23 private def verbatim: Parser[String] =
3.24 {
3.25 - "{*" ~ rep(many1(sym => sym != "*" && Symbol.is_closed(sym)) | """\*(?!\})""".r) ~ "*}" ^^
3.26 + "{*" ~ rep(many1(sym => sym != "*" && Symbol.is_wellformed(sym)) | """\*(?!\})""".r) ~ "*}" ^^
3.27 { case x ~ ys ~ z => x + ys.mkString + z }
3.28 }.named("verbatim")
3.29
3.30 @@ -219,7 +219,7 @@
3.31 def comment: Parser[String] = new Parser[String]
3.32 {
3.33 val comment_text =
3.34 - rep(many1(sym => sym != "*" && sym != "(" && Symbol.is_closed(sym)) |
3.35 + rep(many1(sym => sym != "*" && sym != "(" && Symbol.is_wellformed(sym)) |
3.36 """\*(?!\))|\((?!\*)""".r)
3.37 val comment_open = "(*" ~ comment_text ^^^ ()
3.38 val comment_close = comment_text ~ "*)" ^^^ ()
3.39 @@ -276,7 +276,7 @@
3.40
3.41 val sym_ident =
3.42 (many1(symbols.is_symbolic_char) |
3.43 - one(sym => symbols.is_symbolic(sym) & Symbol.is_closed(sym))) ^^
3.44 + one(sym => symbols.is_symbolic(sym) & Symbol.is_wellformed(sym))) ^^
3.45 (x => Token(Token_Kind.SYM_IDENT, x))
3.46
3.47 val space = many1(symbols.is_blank) ^^ (x => Token(Token_Kind.SPACE, x))
4.1 --- a/src/Pure/General/symbol.scala Mon Jan 11 16:45:02 2010 +0100
4.2 +++ b/src/Pure/General/symbol.scala Mon Jan 11 23:11:31 2010 +0100
4.3 @@ -23,6 +23,8 @@
4.4 \^? [A-Za-z][A-Za-z0-9_']* |
4.5 \^raw: [\x20-\x7e\u0100-\uffff && [^.>]]* ) >""")
4.6
4.7 + // FIXME cover bad surrogates!?
4.8 + // FIXME check wrt. ML version
4.9 private val bad_symbol = new Regex("(?xs) (?!" + symbol + ")" +
4.10 """ \\ < (?: (?! \s | [\"`\\] | \(\* | \*\) | \{\* | \*\} ) . )*""")
4.11
4.12 @@ -32,14 +34,10 @@
4.13
4.14 /* basic matching */
4.15
4.16 - def is_closed(c: Char): Boolean =
4.17 - !(c == '\\' || Character.isHighSurrogate(c))
4.18 + def is_plain(c: Char): Boolean = !(c == '\\' || '\ud800' <= c && c <= '\udfff')
4.19
4.20 - def is_closed(s: CharSequence): Boolean =
4.21 - {
4.22 - if (s.length == 1) is_closed(s.charAt(0))
4.23 - else !bad_symbol.pattern.matcher(s).matches
4.24 - }
4.25 + def is_wellformed(s: CharSequence): Boolean =
4.26 + s.length == 1 && is_plain(s.charAt(0)) || !bad_symbol.pattern.matcher(s).matches
4.27
4.28 class Matcher(text: CharSequence)
4.29 {
4.30 @@ -47,7 +45,7 @@
4.31 def apply(start: Int, end: Int): Int =
4.32 {
4.33 require(0 <= start && start < end && end <= text.length)
4.34 - if (is_closed(text.charAt(start))) 1
4.35 + if (is_plain(text.charAt(start))) 1
4.36 else {
4.37 matcher.region(start, end).lookingAt
4.38 matcher.group.length
4.39 @@ -177,7 +175,7 @@
4.40 }
4.41 }
4.42 decl.split("\\s+").toList match {
4.43 - case sym :: props if sym.length > 1 && is_closed(sym) => (sym, read_props(props))
4.44 + case sym :: props if sym.length > 1 && is_wellformed(sym) => (sym, read_props(props))
4.45 case _ => err()
4.46 }
4.47 }
5.1 --- a/src/Pure/General/xml.scala Mon Jan 11 16:45:02 2010 +0100
5.2 +++ b/src/Pure/General/xml.scala Mon Jan 11 23:11:31 2010 +0100
5.3 @@ -10,8 +10,6 @@
5.4 import java.lang.ref.WeakReference
5.5 import javax.xml.parsers.DocumentBuilderFactory
5.6
5.7 -import org.w3c.dom.{Node, Document}
5.8 -
5.9
5.10 object XML
5.11 {
5.12 @@ -151,15 +149,15 @@
5.13
5.14 /* document object model (W3C DOM) */
5.15
5.16 - def get_data(node: Node): Option[XML.Tree] =
5.17 + def get_data(node: org.w3c.dom.Node): Option[XML.Tree] =
5.18 node.getUserData(Markup.DATA) match {
5.19 case tree: XML.Tree => Some(tree)
5.20 case _ => None
5.21 }
5.22
5.23 - def document_node(doc: Document, tree: Tree): Node =
5.24 + def document_node(doc: org.w3c.dom.Document, tree: Tree): org.w3c.dom.Node =
5.25 {
5.26 - def DOM(tr: Tree): Node = tr match {
5.27 + def DOM(tr: Tree): org.w3c.dom.Node = tr match {
5.28 case Elem(Markup.DATA, Nil, List(data, t)) =>
5.29 val node = DOM(t)
5.30 node.setUserData(Markup.DATA, data, null)
6.1 --- a/src/Pure/Isar/outer_lex.scala Mon Jan 11 16:45:02 2010 +0100
6.2 +++ b/src/Pure/Isar/outer_lex.scala Mon Jan 11 23:11:31 2010 +0100
6.3 @@ -48,7 +48,7 @@
6.4 def is_text: Boolean = is_xname || kind == Token_Kind.VERBATIM
6.5 def is_space: Boolean = kind == Token_Kind.SPACE
6.6 def is_comment: Boolean = kind == Token_Kind.COMMENT
6.7 - def is_proper: Boolean = !(is_space || is_comment)
6.8 + def is_ignored: Boolean = is_space || is_comment
6.9 def is_unparsed: Boolean = kind == Token_Kind.UNPARSED
6.10
6.11 def content: String =
7.1 --- a/src/Pure/Isar/outer_parse.scala Mon Jan 11 16:45:02 2010 +0100
7.2 +++ b/src/Pure/Isar/outer_parse.scala Mon Jan 11 23:11:31 2010 +0100
7.3 @@ -20,7 +20,7 @@
7.4 def filter_proper = true
7.5
7.6 private def proper(in: Input): Input =
7.7 - if (in.atEnd || in.first.is_proper || !filter_proper) in
7.8 + if (in.atEnd || !in.first.is_ignored || !filter_proper) in
7.9 else proper(in.rest)
7.10
7.11 def token(s: String, pred: Elem => Boolean): Parser[Elem] = new Parser[Elem]
8.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
8.2 +++ b/src/Pure/System/session.scala Mon Jan 11 23:11:31 2010 +0100
8.3 @@ -0,0 +1,250 @@
8.4 +/*
8.5 + * Isabelle session, potentially with running prover
8.6 + *
8.7 + * @author Makarius
8.8 + */
8.9 +
8.10 +package isabelle
8.11 +
8.12 +
8.13 +import scala.actors.TIMEOUT
8.14 +import scala.actors.Actor._
8.15 +
8.16 +
8.17 +object Session
8.18 +{
8.19 + /* events */
8.20 +
8.21 + case object Global_Settings
8.22 +
8.23 +
8.24 + /* managed entities */
8.25 +
8.26 + type Entity_ID = String
8.27 +
8.28 + trait Entity
8.29 + {
8.30 + val id: Entity_ID
8.31 + def consume(session: Session, message: XML.Tree): Unit
8.32 + }
8.33 +}
8.34 +
8.35 +
8.36 +class Session(system: Isabelle_System)
8.37 +{
8.38 + /* pervasive event buses */
8.39 +
8.40 + val global_settings = new Event_Bus[Session.Global_Settings.type]
8.41 + val raw_results = new Event_Bus[Isabelle_Process.Result]
8.42 + val results = new Event_Bus[Command]
8.43 +
8.44 + val command_change = new Event_Bus[Command]
8.45 +
8.46 +
8.47 + /* unique ids */
8.48 +
8.49 + private var id_count: BigInt = 0
8.50 + def create_id(): Session.Entity_ID = synchronized { id_count += 1; "j" + id_count }
8.51 +
8.52 +
8.53 +
8.54 + /** main actor **/
8.55 +
8.56 + @volatile private var syntax = new Outer_Syntax(system.symbols)
8.57 + def current_syntax: Outer_Syntax = syntax
8.58 +
8.59 + @volatile private var entities = Map[Session.Entity_ID, Session.Entity]()
8.60 + def lookup_entity(id: Session.Entity_ID): Option[Session.Entity] = entities.get(id)
8.61 + def lookup_command(id: Session.Entity_ID): Option[Command] =
8.62 + lookup_entity(id) match {
8.63 + case Some(cmd: Command) => Some(cmd)
8.64 + case _ => None
8.65 + }
8.66 +
8.67 + private case class Start(timeout: Int, args: List[String])
8.68 + private case object Stop
8.69 + private case class Begin_Document(path: String)
8.70 +
8.71 + private val session_actor = actor {
8.72 +
8.73 + var prover: Isabelle_Process with Isar_Document = null
8.74 +
8.75 + def register(entity: Session.Entity) { entities += (entity.id -> entity) }
8.76 +
8.77 + var documents = Map[Isar_Document.Document_ID, Document]()
8.78 + def register_document(doc: Document) { documents += (doc.id -> doc) }
8.79 +
8.80 +
8.81 + /* document changes */
8.82 +
8.83 + def handle_change(change: Change)
8.84 + {
8.85 + require(change.parent.isDefined)
8.86 +
8.87 + val (changes, doc) = change.result.join
8.88 + val id_changes = changes map {
8.89 + case (c1, c2) =>
8.90 + (c1.map(_.id).getOrElse(""),
8.91 + c2 match {
8.92 + case None => None
8.93 + case Some(command) =>
8.94 + if (!lookup_command(command.id).isDefined) {
8.95 + register(command)
8.96 + prover.define_command(command.id, system.symbols.encode(command.source))
8.97 + }
8.98 + Some(command.id)
8.99 + })
8.100 + }
8.101 + register_document(doc)
8.102 + prover.edit_document(change.parent.get.id, doc.id, id_changes)
8.103 + }
8.104 +
8.105 +
8.106 + /* prover results */
8.107 +
8.108 + def bad_result(result: Isabelle_Process.Result)
8.109 + {
8.110 + System.err.println("Ignoring prover result: " + result)
8.111 + }
8.112 +
8.113 + def handle_result(result: Isabelle_Process.Result)
8.114 + {
8.115 + raw_results.event(result)
8.116 +
8.117 + val target_id: Option[Session.Entity_ID] = Position.get_id(result.props)
8.118 + val target: Option[Session.Entity] =
8.119 + target_id match {
8.120 + case None => None
8.121 + case Some(id) => lookup_entity(id)
8.122 + }
8.123 + if (target.isDefined) target.get.consume(this, result.message)
8.124 + else if (result.kind == Isabelle_Process.Kind.STATUS) {
8.125 + // global status message
8.126 + result.body match {
8.127 +
8.128 + // document state assigment
8.129 + case List(XML.Elem(Markup.ASSIGN, _, edits)) if target_id.isDefined =>
8.130 + documents.get(target_id.get) match {
8.131 + case Some(doc) =>
8.132 + val states =
8.133 + for {
8.134 + XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _)
8.135 + <- edits
8.136 + cmd <- lookup_command(cmd_id)
8.137 + } yield {
8.138 + val st = cmd.assign_state(state_id)
8.139 + register(st)
8.140 + (cmd, st)
8.141 + }
8.142 + doc.assign_states(states)
8.143 + case None => bad_result(result)
8.144 + }
8.145 +
8.146 + // command and keyword declarations
8.147 + case List(XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _)) =>
8.148 + syntax += (name, kind)
8.149 + case List(XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _)) =>
8.150 + syntax += name
8.151 +
8.152 + case _ => if (!result.is_ready) bad_result(result)
8.153 + }
8.154 + }
8.155 + else if (result.kind == Isabelle_Process.Kind.EXIT)
8.156 + prover = null
8.157 + else if (result.kind != Isabelle_Process.Kind.STDIN && !result.is_raw)
8.158 + bad_result(result)
8.159 + }
8.160 +
8.161 +
8.162 + /* prover startup */
8.163 +
8.164 + def startup_error(): String =
8.165 + {
8.166 + val buf = new StringBuilder
8.167 + while (
8.168 + receiveWithin(0) {
8.169 + case result: Isabelle_Process.Result =>
8.170 + if (result.is_raw) {
8.171 + for (text <- XML.content(result.message))
8.172 + buf.append(text)
8.173 + }
8.174 + true
8.175 + case TIMEOUT => false
8.176 + }) {}
8.177 + buf.toString
8.178 + }
8.179 +
8.180 + def prover_startup(timeout: Int): Option[String] =
8.181 + {
8.182 + receiveWithin(timeout) {
8.183 + case result: Isabelle_Process.Result
8.184 + if result.kind == Isabelle_Process.Kind.INIT =>
8.185 + while (receive {
8.186 + case result: Isabelle_Process.Result =>
8.187 + handle_result(result); !result.is_ready
8.188 + }) {}
8.189 + None
8.190 +
8.191 + case result: Isabelle_Process.Result
8.192 + if result.kind == Isabelle_Process.Kind.EXIT =>
8.193 + Some(startup_error())
8.194 +
8.195 + case TIMEOUT => // FIXME clarify
8.196 + prover.kill; Some(startup_error())
8.197 + }
8.198 + }
8.199 +
8.200 +
8.201 + /* main loop */
8.202 +
8.203 + val xml_cache = new XML.Cache(131071)
8.204 +
8.205 + loop {
8.206 + react {
8.207 + case Start(timeout, args) =>
8.208 + if (prover == null) {
8.209 + prover = new Isabelle_Process(system, self, args:_*) with Isar_Document
8.210 + val origin = sender
8.211 + val opt_err = prover_startup(timeout)
8.212 + if (opt_err.isDefined) prover = null
8.213 + origin ! opt_err
8.214 + }
8.215 + else reply(None)
8.216 +
8.217 + case Stop => // FIXME clarify; synchronous
8.218 + if (prover != null) {
8.219 + prover.kill
8.220 + prover = null
8.221 + }
8.222 +
8.223 + case Begin_Document(path: String) if prover != null =>
8.224 + val id = create_id()
8.225 + val doc = Document.empty(id)
8.226 + register_document(doc)
8.227 + prover.begin_document(id, path)
8.228 + reply(doc)
8.229 +
8.230 + case change: Change if prover != null =>
8.231 + handle_change(change)
8.232 +
8.233 + case result: Isabelle_Process.Result =>
8.234 + handle_result(result.cache(xml_cache))
8.235 +
8.236 + case bad if prover != null =>
8.237 + System.err.println("session_actor: ignoring bad message " + bad)
8.238 + }
8.239 + }
8.240 + }
8.241 +
8.242 +
8.243 + /* main methods */
8.244 +
8.245 + def start(timeout: Int, args: List[String]): Option[String] =
8.246 + (session_actor !? Start(timeout, args)).asInstanceOf[Option[String]]
8.247 +
8.248 + def stop() { session_actor ! Stop }
8.249 + def input(change: Change) { session_actor ! change }
8.250 +
8.251 + def begin_document(path: String): Document =
8.252 + (session_actor !? Begin_Document(path)).asInstanceOf[Document]
8.253 +}
9.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
9.2 +++ b/src/Pure/Thy/change.scala Mon Jan 11 23:11:31 2010 +0100
9.3 @@ -0,0 +1,42 @@
9.4 +/*
9.5 + * Changes of plain text
9.6 + *
9.7 + * @author Fabian Immler, TU Munich
9.8 + * @author Makarius
9.9 + */
9.10 +
9.11 +package isabelle
9.12 +
9.13 +
9.14 +class Change(
9.15 + val id: Isar_Document.Document_ID,
9.16 + val parent: Option[Change],
9.17 + val edits: List[Text_Edit],
9.18 + val result: Future[(List[Document.Edit], Document)])
9.19 +{
9.20 + def ancestors: Iterator[Change] = new Iterator[Change]
9.21 + {
9.22 + private var state: Option[Change] = Some(Change.this)
9.23 + def hasNext = state.isDefined
9.24 + def next =
9.25 + state match {
9.26 + case Some(change) => state = change.parent; change
9.27 + case None => throw new NoSuchElementException("next on empty iterator")
9.28 + }
9.29 + }
9.30 +
9.31 + def join_document: Document = result.join._2
9.32 + def is_assigned: Boolean = result.is_finished && join_document.assignment.is_finished
9.33 +
9.34 + def edit(session: Session, edits: List[Text_Edit]): Change =
9.35 + {
9.36 + val new_id = session.create_id()
9.37 + val result: Future[(List[Document.Edit], Document)] =
9.38 + Future.fork {
9.39 + val old_doc = join_document
9.40 + old_doc.await_assignment
9.41 + Document.text_edits(session, old_doc, new_id, edits)
9.42 + }
9.43 + new Change(new_id, Some(this), edits, result)
9.44 + }
9.45 +}
9.46 \ No newline at end of file
10.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
10.2 +++ b/src/Pure/Thy/command.scala Mon Jan 11 23:11:31 2010 +0100
10.3 @@ -0,0 +1,100 @@
10.4 +/*
10.5 + * Prover commands with semantic state
10.6 + *
10.7 + * @author Johannes Hölzl, TU Munich
10.8 + * @author Fabian Immler, TU Munich
10.9 + */
10.10 +
10.11 +package isabelle
10.12 +
10.13 +
10.14 +import scala.actors.Actor, Actor._
10.15 +import scala.collection.mutable
10.16 +
10.17 +
10.18 +object Command
10.19 +{
10.20 + object Status extends Enumeration
10.21 + {
10.22 + val UNPROCESSED = Value("UNPROCESSED")
10.23 + val FINISHED = Value("FINISHED")
10.24 + val FAILED = Value("FAILED")
10.25 + }
10.26 +
10.27 + case class HighlightInfo(highlight: String) { override def toString = highlight }
10.28 + case class TypeInfo(ty: String)
10.29 + case class RefInfo(file: Option[String], line: Option[Int],
10.30 + command_id: Option[String], offset: Option[Int])
10.31 +}
10.32 +
10.33 +
10.34 +class Command(
10.35 + val id: Isar_Document.Command_ID,
10.36 + val span: Thy_Syntax.Span)
10.37 + extends Session.Entity
10.38 +{
10.39 + /* classification */
10.40 +
10.41 + def is_command: Boolean = !span.isEmpty && span.first.is_command
10.42 + def is_ignored: Boolean = span.forall(_.is_ignored)
10.43 + def is_malformed: Boolean = !is_command && !is_ignored
10.44 +
10.45 + def name: String = if (is_command) span.first.content else ""
10.46 + override def toString = if (is_command) name else if (is_ignored) "<ignored>" else "<malformed>"
10.47 +
10.48 +
10.49 + /* source text */
10.50 +
10.51 + val source: String = span.map(_.source).mkString
10.52 + def source(i: Int, j: Int): String = source.substring(i, j)
10.53 + def length: Int = source.length
10.54 +
10.55 + lazy val symbol_index = new Symbol.Index(source)
10.56 +
10.57 +
10.58 + /* accumulated messages */
10.59 +
10.60 + @volatile protected var state = new State(this)
10.61 + def current_state: State = state
10.62 +
10.63 + private case class Consume(session: Session, message: XML.Tree)
10.64 + private case object Assign
10.65 +
10.66 + private val accumulator = actor {
10.67 + var assigned = false
10.68 + loop {
10.69 + react {
10.70 + case Consume(session: Session, message: XML.Tree) if !assigned =>
10.71 + state = state.+(session, message)
10.72 +
10.73 + case Assign =>
10.74 + assigned = true // single assignment
10.75 + reply(())
10.76 +
10.77 + case bad => System.err.println("command accumulator: ignoring bad message " + bad)
10.78 + }
10.79 + }
10.80 + }
10.81 +
10.82 + def consume(session: Session, message: XML.Tree) { accumulator ! Consume(session, message) }
10.83 +
10.84 + def assign_state(state_id: Isar_Document.State_ID): Command =
10.85 + {
10.86 + val cmd = new Command(state_id, span)
10.87 + accumulator !? Assign
10.88 + cmd.state = current_state
10.89 + cmd
10.90 + }
10.91 +
10.92 +
10.93 + /* markup */
10.94 +
10.95 + lazy val empty_markup = new Markup_Text(Nil, source)
10.96 +
10.97 + def markup_node(begin: Int, end: Int, info: Any): Markup_Tree =
10.98 + {
10.99 + val start = symbol_index.decode(begin)
10.100 + val stop = symbol_index.decode(end)
10.101 + new Markup_Tree(new Markup_Node(start, stop, info), Nil)
10.102 + }
10.103 +}
11.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
11.2 +++ b/src/Pure/Thy/document.scala Mon Jan 11 23:11:31 2010 +0100
11.3 @@ -0,0 +1,197 @@
11.4 +/*
11.5 + * Document as editable list of commands
11.6 + *
11.7 + * @author Makarius
11.8 + */
11.9 +
11.10 +package isabelle
11.11 +
11.12 +
11.13 +object Document
11.14 +{
11.15 + /* command start positions */
11.16 +
11.17 + def command_starts(commands: Linear_Set[Command]): Iterator[(Command, Int)] =
11.18 + {
11.19 + var offset = 0
11.20 + for (cmd <- commands.elements) yield {
11.21 + val start = offset
11.22 + offset += cmd.length
11.23 + (cmd, start)
11.24 + }
11.25 + }
11.26 +
11.27 +
11.28 + /* empty document */
11.29 +
11.30 + def empty(id: Isar_Document.Document_ID): Document =
11.31 + {
11.32 + val doc = new Document(id, Linear_Set(), Map())
11.33 + doc.assign_states(Nil)
11.34 + doc
11.35 + }
11.36 +
11.37 +
11.38 + // FIXME
11.39 + var phase0: List[Text_Edit] = null
11.40 + var phase1: Linear_Set[Command] = null
11.41 + var phase2: Linear_Set[Command] = null
11.42 + var phase3: List[Edit] = null
11.43 +
11.44 +
11.45 +
11.46 + /** document edits **/
11.47 +
11.48 + type Edit = (Option[Command], Option[Command])
11.49 +
11.50 + def text_edits(session: Session, old_doc: Document, new_id: Isar_Document.Document_ID,
11.51 + edits: List[Text_Edit]): (List[Edit], Document) =
11.52 + {
11.53 + require(old_doc.assignment.is_finished)
11.54 +
11.55 +
11.56 + /* unparsed dummy commands */
11.57 +
11.58 + def unparsed(source: String) =
11.59 + new Command(null, List(Outer_Lex.Token(Outer_Lex.Token_Kind.UNPARSED, source)))
11.60 +
11.61 + def is_unparsed(command: Command) = command.id == null
11.62 +
11.63 + assert(!old_doc.commands.exists(is_unparsed)) // FIXME remove
11.64 +
11.65 +
11.66 + /* phase 1: edit individual command source */
11.67 +
11.68 + def edit_text(eds: List[Text_Edit], commands: Linear_Set[Command]): Linear_Set[Command] =
11.69 + {
11.70 + eds match {
11.71 + case e :: es =>
11.72 + command_starts(commands).find { // FIXME relative search!
11.73 + case (cmd, cmd_start) =>
11.74 + e.can_edit(cmd.source, cmd_start) || e.is_insert && e.start == cmd_start + cmd.length
11.75 + } match {
11.76 + case Some((cmd, cmd_start)) if e.can_edit(cmd.source, cmd_start) =>
11.77 + val (rest, text) = e.edit(cmd.source, cmd_start)
11.78 + val new_commands = commands.insert_after(Some(cmd), unparsed(text)) - cmd
11.79 + edit_text(rest.toList ::: es, new_commands)
11.80 +
11.81 + case Some((cmd, cmd_start)) =>
11.82 + edit_text(es, commands.insert_after(Some(cmd), unparsed(e.text)))
11.83 +
11.84 + case None =>
11.85 + require(e.is_insert && e.start == 0)
11.86 + edit_text(es, commands.insert_after(None, unparsed(e.text)))
11.87 + }
11.88 + case Nil => commands
11.89 + }
11.90 + }
11.91 +
11.92 +
11.93 + /* phase 2: recover command spans */
11.94 +
11.95 + def parse_spans(commands: Linear_Set[Command]): Linear_Set[Command] =
11.96 + {
11.97 + // FIXME relative search!
11.98 + commands.elements.find(is_unparsed) match {
11.99 + case Some(first_unparsed) =>
11.100 + val prefix = commands.prev(first_unparsed)
11.101 + val body = commands.elements(first_unparsed).takeWhile(is_unparsed).toList
11.102 + val suffix = commands.next(body.last)
11.103 +
11.104 + val sources = (prefix.toList ::: body ::: suffix.toList).flatMap(_.span.map(_.source))
11.105 + val spans0 = Thy_Syntax.parse_spans(session.current_syntax.scan(sources.mkString))
11.106 +
11.107 + val (before_edit, spans1) =
11.108 + if (!spans0.isEmpty && Some(spans0.first) == prefix.map(_.span))
11.109 + (prefix, spans0.tail)
11.110 + else (if (prefix.isDefined) commands.prev(prefix.get) else None, spans0)
11.111 +
11.112 + val (after_edit, spans2) =
11.113 + if (!spans1.isEmpty && Some(spans1.last) == suffix.map(_.span))
11.114 + (suffix, spans1.take(spans1.length - 1))
11.115 + else (if (suffix.isDefined) commands.next(suffix.get) else None, spans1)
11.116 +
11.117 + val inserted = spans2.map(span => new Command(session.create_id(), span))
11.118 + val new_commands =
11.119 + commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted)
11.120 + parse_spans(new_commands)
11.121 +
11.122 + case None => commands
11.123 + }
11.124 + }
11.125 +
11.126 +
11.127 + /* phase 3: resulting document edits */
11.128 +
11.129 + val result = Library.timeit("text_edits") {
11.130 + val commands0 = old_doc.commands
11.131 + val commands1 = Library.timeit("edit_text") { edit_text(edits, commands0) }
11.132 + val commands2 = Library.timeit("parse_spans") { parse_spans(commands1) }
11.133 +
11.134 + val removed_commands = commands0.elements.filter(!commands2.contains(_)).toList
11.135 + val inserted_commands = commands2.elements.filter(!commands0.contains(_)).toList
11.136 +
11.137 + val doc_edits =
11.138 + removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
11.139 + inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
11.140 +
11.141 + val former_states = old_doc.assignment.join -- removed_commands
11.142 +
11.143 + phase0 = edits
11.144 + phase1 = commands1
11.145 + phase2 = commands2
11.146 + phase3 = doc_edits
11.147 +
11.148 + (doc_edits, new Document(new_id, commands2, former_states))
11.149 + }
11.150 + result
11.151 + }
11.152 +}
11.153 +
11.154 +
11.155 +class Document(
11.156 + val id: Isar_Document.Document_ID,
11.157 + val commands: Linear_Set[Command],
11.158 + former_states: Map[Command, Command])
11.159 +{
11.160 + /* command ranges */
11.161 +
11.162 + def command_starts: Iterator[(Command, Int)] = Document.command_starts(commands)
11.163 +
11.164 + def command_start(cmd: Command): Option[Int] =
11.165 + command_starts.find(_._1 == cmd).map(_._2)
11.166 +
11.167 + def command_range(i: Int): Iterator[(Command, Int)] =
11.168 + command_starts dropWhile { case (cmd, start) => start + cmd.length <= i }
11.169 +
11.170 + def command_range(i: Int, j: Int): Iterator[(Command, Int)] =
11.171 + command_range(i) takeWhile { case (_, start) => start < j }
11.172 +
11.173 + def command_at(i: Int): Option[(Command, Int)] =
11.174 + {
11.175 + val range = command_range(i)
11.176 + if (range.hasNext) Some(range.next) else None
11.177 + }
11.178 +
11.179 +
11.180 + /* command state assignment */
11.181 +
11.182 + val assignment = Future.promise[Map[Command, Command]]
11.183 + def await_assignment { assignment.join }
11.184 +
11.185 + @volatile private var tmp_states = former_states
11.186 + private val time0 = System.currentTimeMillis
11.187 +
11.188 + def assign_states(new_states: List[(Command, Command)])
11.189 + {
11.190 + assignment.fulfill(tmp_states ++ new_states)
11.191 + tmp_states = Map()
11.192 + System.err.println("assign_states: " + (System.currentTimeMillis - time0) + " ms elapsed time")
11.193 + }
11.194 +
11.195 + def current_state(cmd: Command): Option[State] =
11.196 + {
11.197 + require(assignment.is_finished)
11.198 + (assignment.join).get(cmd).map(_.current_state)
11.199 + }
11.200 +}
12.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
12.2 +++ b/src/Pure/Thy/markup_node.scala Mon Jan 11 23:11:31 2010 +0100
12.3 @@ -0,0 +1,111 @@
12.4 +/*
12.5 + * Document markup nodes, with connection to Swing tree model
12.6 + *
12.7 + * @author Fabian Immler, TU Munich
12.8 + * @author Makarius
12.9 + */
12.10 +
12.11 +package isabelle
12.12 +
12.13 +
12.14 +import javax.swing.tree.DefaultMutableTreeNode
12.15 +
12.16 +
12.17 +
12.18 +class Markup_Node(val start: Int, val stop: Int, val info: Any)
12.19 +{
12.20 + def fits_into(that: Markup_Node): Boolean =
12.21 + that.start <= this.start && this.stop <= that.stop
12.22 +}
12.23 +
12.24 +
12.25 +class Markup_Tree(val node: Markup_Node, val branches: List[Markup_Tree])
12.26 +{
12.27 + def set_branches(bs: List[Markup_Tree]): Markup_Tree = new Markup_Tree(node, bs)
12.28 +
12.29 + private def add(branch: Markup_Tree) = // FIXME avoid sort
12.30 + set_branches((branch :: branches) sort ((a, b) => a.node.start < b.node.start))
12.31 +
12.32 + private def remove(bs: List[Markup_Tree]) = set_branches(branches -- bs)
12.33 +
12.34 + def + (new_tree: Markup_Tree): Markup_Tree =
12.35 + {
12.36 + val new_node = new_tree.node
12.37 + if (new_node fits_into node) {
12.38 + var inserted = false
12.39 + val new_branches =
12.40 + branches.map(branch =>
12.41 + if ((new_node fits_into branch.node) && !inserted) {
12.42 + inserted = true
12.43 + branch + new_tree
12.44 + }
12.45 + else branch)
12.46 + if (!inserted) {
12.47 + // new_tree did not fit into children of this
12.48 + // -> insert between this and its branches
12.49 + val fitting = branches filter(_.node fits_into new_node)
12.50 + (this remove fitting) add ((new_tree /: fitting)(_ + _))
12.51 + }
12.52 + else set_branches(new_branches)
12.53 + }
12.54 + else {
12.55 + System.err.println("ignored nonfitting markup: " + new_node)
12.56 + this
12.57 + }
12.58 + }
12.59 +
12.60 + def flatten: List[Markup_Node] =
12.61 + {
12.62 + var next_x = node.start
12.63 + if (branches.isEmpty) List(this.node)
12.64 + else {
12.65 + val filled_gaps =
12.66 + for {
12.67 + child <- branches
12.68 + markups =
12.69 + if (next_x < child.node.start)
12.70 + new Markup_Node(next_x, child.node.start, node.info) :: child.flatten
12.71 + else child.flatten
12.72 + update = (next_x = child.node.stop)
12.73 + markup <- markups
12.74 + } yield markup
12.75 + if (next_x < node.stop)
12.76 + filled_gaps + new Markup_Node(next_x, node.stop, node.info)
12.77 + else filled_gaps
12.78 + }
12.79 + }
12.80 +}
12.81 +
12.82 +
12.83 +class Markup_Text(val markup: List[Markup_Tree], val content: String)
12.84 +{
12.85 + private lazy val root =
12.86 + new Markup_Tree(new Markup_Node(0, content.length, None), markup)
12.87 +
12.88 + def + (new_tree: Markup_Tree): Markup_Text =
12.89 + new Markup_Text((root + new_tree).branches, content)
12.90 +
12.91 + def filter(pred: Markup_Node => Boolean): Markup_Text =
12.92 + {
12.93 + def filt(tree: Markup_Tree): List[Markup_Tree] =
12.94 + {
12.95 + val branches = tree.branches.flatMap(filt(_))
12.96 + if (pred(tree.node)) List(tree.set_branches(branches))
12.97 + else branches
12.98 + }
12.99 + new Markup_Text(markup.flatMap(filt(_)), content)
12.100 + }
12.101 +
12.102 + def flatten: List[Markup_Node] = markup.flatten(_.flatten)
12.103 +
12.104 + def swing_tree(swing_node: Markup_Node => DefaultMutableTreeNode): DefaultMutableTreeNode =
12.105 + {
12.106 + def swing(tree: Markup_Tree): DefaultMutableTreeNode =
12.107 + {
12.108 + val node = swing_node(tree.node)
12.109 + tree.branches foreach ((branch: Markup_Tree) => node.add(swing(branch)))
12.110 + node
12.111 + }
12.112 + swing(root)
12.113 + }
12.114 +}
13.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
13.2 +++ b/src/Pure/Thy/state.scala Mon Jan 11 23:11:31 2010 +0100
13.3 @@ -0,0 +1,117 @@
13.4 +/*
13.5 + * Accumulating results from prover
13.6 + *
13.7 + * @author Fabian Immler, TU Munich
13.8 + * @author Makarius
13.9 + */
13.10 +
13.11 +package isabelle
13.12 +
13.13 +
13.14 +class State(
13.15 + val command: Command,
13.16 + val status: Command.Status.Value,
13.17 + val rev_results: List[XML.Tree],
13.18 + val markup_root: Markup_Text)
13.19 +{
13.20 + def this(command: Command) =
13.21 + this(command, Command.Status.UNPROCESSED, Nil, command.empty_markup)
13.22 +
13.23 +
13.24 + /* content */
13.25 +
13.26 + private def set_status(st: Command.Status.Value): State =
13.27 + new State(command, st, rev_results, markup_root)
13.28 +
13.29 + private def add_result(res: XML.Tree): State =
13.30 + new State(command, status, res :: rev_results, markup_root)
13.31 +
13.32 + private def add_markup(node: Markup_Tree): State =
13.33 + new State(command, status, rev_results, markup_root + node)
13.34 +
13.35 + lazy val results = rev_results.reverse
13.36 +
13.37 +
13.38 + /* markup */
13.39 +
13.40 + lazy val highlight: Markup_Text =
13.41 + {
13.42 + markup_root.filter(_.info match {
13.43 + case Command.HighlightInfo(_) => true
13.44 + case _ => false
13.45 + })
13.46 + }
13.47 +
13.48 + private lazy val types: List[Markup_Node] =
13.49 + markup_root.filter(_.info match {
13.50 + case Command.TypeInfo(_) => true
13.51 + case _ => false }).flatten
13.52 +
13.53 + def type_at(pos: Int): Option[String] =
13.54 + {
13.55 + types.find(t => t.start <= pos && pos < t.stop) match {
13.56 + case Some(t) =>
13.57 + t.info match {
13.58 + case Command.TypeInfo(ty) => Some(command.source(t.start, t.stop) + ": " + ty)
13.59 + case _ => None
13.60 + }
13.61 + case None => None
13.62 + }
13.63 + }
13.64 +
13.65 + private lazy val refs: List[Markup_Node] =
13.66 + markup_root.filter(_.info match {
13.67 + case Command.RefInfo(_, _, _, _) => true
13.68 + case _ => false }).flatten
13.69 +
13.70 + def ref_at(pos: Int): Option[Markup_Node] =
13.71 + refs.find(t => t.start <= pos && pos < t.stop)
13.72 +
13.73 +
13.74 + /* message dispatch */
13.75 +
13.76 + def + (session: Session, message: XML.Tree): State =
13.77 + {
13.78 + val changed: State =
13.79 + message match {
13.80 + case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.STATUS) :: _, elems) =>
13.81 + (this /: elems)((state, elem) =>
13.82 + elem match {
13.83 + case XML.Elem(Markup.UNPROCESSED, _, _) => state.set_status(Command.Status.UNPROCESSED)
13.84 + case XML.Elem(Markup.FINISHED, _, _) => state.set_status(Command.Status.FINISHED)
13.85 + case XML.Elem(Markup.FAILED, _, _) => state.set_status(Command.Status.FAILED)
13.86 + case XML.Elem(kind, atts, body) =>
13.87 + val (begin, end) = Position.get_offsets(atts)
13.88 + if (begin.isEmpty || end.isEmpty) state
13.89 + else if (kind == Markup.ML_TYPING) {
13.90 + val info = body.first.asInstanceOf[XML.Text].content // FIXME proper match!?
13.91 + state.add_markup(
13.92 + command.markup_node(begin.get - 1, end.get - 1, Command.TypeInfo(info)))
13.93 + }
13.94 + else if (kind == Markup.ML_REF) {
13.95 + body match {
13.96 + case List(XML.Elem(Markup.ML_DEF, atts, _)) =>
13.97 + state.add_markup(command.markup_node(
13.98 + begin.get - 1, end.get - 1,
13.99 + Command.RefInfo(
13.100 + Position.get_file(atts),
13.101 + Position.get_line(atts),
13.102 + Position.get_id(atts),
13.103 + Position.get_offset(atts))))
13.104 + case _ => state
13.105 + }
13.106 + }
13.107 + else {
13.108 + state.add_markup(
13.109 + command.markup_node(begin.get - 1, end.get - 1, Command.HighlightInfo(kind)))
13.110 + }
13.111 + case _ =>
13.112 + System.err.println("ignored status report: " + elem)
13.113 + state
13.114 + })
13.115 + case _ => add_result(message)
13.116 + }
13.117 + if (!(this eq changed)) session.command_change.event(command)
13.118 + changed
13.119 + }
13.120 +}
14.1 --- a/src/Pure/Thy/text_edit.scala Mon Jan 11 16:45:02 2010 +0100
14.2 +++ b/src/Pure/Thy/text_edit.scala Mon Jan 11 23:11:31 2010 +0100
14.3 @@ -8,72 +8,44 @@
14.4 package isabelle
14.5
14.6
14.7 -sealed abstract class Text_Edit
14.8 +class Text_Edit(val is_insert: Boolean, val start: Int, val text: String)
14.9 {
14.10 - val start: Int
14.11 - def text: String
14.12 - def after(offset: Int): Int
14.13 - def before(offset: Int): Int
14.14 - def can_edit(string_length: Int, shift: Int): Boolean
14.15 - def edit(string: String, shift: Int): (Option[Text_Edit], String)
14.16 -}
14.17 + override def toString =
14.18 + (if (is_insert) "Insert(" else "Remove(") + (start, text).toString + ")"
14.19
14.20
14.21 -object Text_Edit
14.22 -{
14.23 /* transform offsets */
14.24
14.25 - private def after_insert(start: Int, text: String, offset: Int): Int =
14.26 - if (start <= offset) offset + text.length
14.27 - else offset
14.28 + private def transform(do_insert: Boolean, offset: Int): Int =
14.29 + if (offset < start) offset
14.30 + else if (is_insert == do_insert) offset + text.length
14.31 + else (offset - text.length) max start
14.32
14.33 - private def after_remove(start: Int, text: String, offset: Int): Int =
14.34 - if (start > offset) offset
14.35 - else (offset - text.length) max start
14.36 + def after(offset: Int): Int = transform(true, offset)
14.37 + def before(offset: Int): Int = transform(false, offset)
14.38
14.39
14.40 /* edit strings */
14.41
14.42 - private def insert(index: Int, text: String, string: String): String =
14.43 + private def insert(index: Int, string: String): String =
14.44 string.substring(0, index) + text + string.substring(index)
14.45
14.46 private def remove(index: Int, count: Int, string: String): String =
14.47 string.substring(0, index) + string.substring(index + count)
14.48
14.49 + def can_edit(string: String, shift: Int): Boolean =
14.50 + shift <= start && start < shift + string.length
14.51
14.52 - /* explicit edits */
14.53 -
14.54 - case class Insert(start: Int, text: String) extends Text_Edit
14.55 - {
14.56 - def after(offset: Int): Int = after_insert(start, text, offset)
14.57 - def before(offset: Int): Int = after_remove(start, text, offset)
14.58 -
14.59 - def can_edit(string_length: Int, shift: Int): Boolean =
14.60 - shift <= start && start <= shift + string_length
14.61 -
14.62 - def edit(string: String, shift: Int): (Option[Insert], String) =
14.63 - if (can_edit(string.length, shift)) (None, insert(start - shift, text, string))
14.64 - else (Some(this), string)
14.65 - }
14.66 -
14.67 - case class Remove(start: Int, text: String) extends Text_Edit
14.68 - {
14.69 - def after(offset: Int): Int = after_remove(start, text, offset)
14.70 - def before(offset: Int): Int = after_insert(start, text, offset)
14.71 -
14.72 - def can_edit(string_length: Int, shift: Int): Boolean =
14.73 - shift <= start && start < shift + string_length
14.74 -
14.75 - def edit(string: String, shift: Int): (Option[Remove], String) =
14.76 - if (can_edit(string.length, shift)) {
14.77 - val index = start - shift
14.78 - val count = text.length min (string.length - index)
14.79 - val rest =
14.80 - if (count == text.length) None
14.81 - else Some(Remove(start, text.substring(count)))
14.82 - (rest, remove(index, count, string))
14.83 - }
14.84 - else (Some(this), string)
14.85 - }
14.86 + def edit(string: String, shift: Int): (Option[Text_Edit], String) =
14.87 + if (!can_edit(string, shift)) (Some(this), string)
14.88 + else if (is_insert) (None, insert(start - shift, string))
14.89 + else {
14.90 + val index = start - shift
14.91 + val count = text.length min (string.length - index)
14.92 + val rest =
14.93 + if (count == text.length) None
14.94 + else Some(new Text_Edit(false, start, text.substring(count)))
14.95 + (rest, remove(index, count, string))
14.96 + }
14.97 }
14.98
15.1 --- a/src/Pure/Thy/thy_syntax.scala Mon Jan 11 16:45:02 2010 +0100
15.2 +++ b/src/Pure/Thy/thy_syntax.scala Mon Jan 11 23:11:31 2010 +0100
15.3 @@ -15,7 +15,7 @@
15.4
15.5 val command_span: Parser[Span] =
15.6 {
15.7 - val whitespace = token("white space", tok => tok.is_space || tok.is_comment)
15.8 + val whitespace = token("white space", _.is_ignored)
15.9 val command = token("command keyword", _.is_command)
15.10 val body = not(rep(whitespace) ~ (command | eof)) ~> not_eof
15.11 command ~ rep(body) ^^ { case x ~ ys => x :: ys } | rep1(whitespace) | rep1(body)
16.1 --- a/src/Pure/build-jars Mon Jan 11 16:45:02 2010 +0100
16.2 +++ b/src/Pure/build-jars Mon Jan 11 23:11:31 2010 +0100
16.3 @@ -45,10 +45,16 @@
16.4 System/isabelle_syntax.scala
16.5 System/isabelle_system.scala
16.6 System/platform.scala
16.7 + System/session.scala
16.8 System/session_manager.scala
16.9 System/standard_system.scala
16.10 + Thy/change.scala
16.11 + Thy/command.scala
16.12 Thy/completion.scala
16.13 + Thy/document.scala
16.14 Thy/html.scala
16.15 + Thy/markup_node.scala
16.16 + Thy/state.scala
16.17 Thy/text_edit.scala
16.18 Thy/thy_header.scala
16.19 Thy/thy_syntax.scala
17.1 --- a/src/Pure/library.scala Mon Jan 11 16:45:02 2010 +0100
17.2 +++ b/src/Pure/library.scala Mon Jan 11 23:11:31 2010 +0100
17.3 @@ -55,12 +55,13 @@
17.4
17.5 /* timing */
17.6
17.7 - def timeit[A](e: => A) =
17.8 + def timeit[A](message: String)(e: => A) =
17.9 {
17.10 val start = System.currentTimeMillis()
17.11 val result = Exn.capture(e)
17.12 val stop = System.currentTimeMillis()
17.13 - System.err.println((stop - start) + "ms elapsed time")
17.14 + System.err.println(
17.15 + (if (message.isEmpty) "" else message + ": ") + (stop - start) + "ms elapsed time")
17.16 Exn.release(result)
17.17 }
17.18 }
18.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
18.2 +++ b/src/Tools/jEdit/README_BUILD Mon Jan 11 23:11:31 2010 +0100
18.3 @@ -0,0 +1,73 @@
18.4 +
18.5 +Requirements to build from sources
18.6 +==================================
18.7 +
18.8 +* Proper Java JRE/JDK from Sun, e.g. 1.6.0_17
18.9 + http://java.sun.com/javase/downloads/index.jsp
18.10 +
18.11 +* Netbeans 6.7
18.12 + http://www.netbeans.org/downloads/index.html
18.13 +
18.14 +* Scala for Netbeans: version 6.7v1 for NB 6.7
18.15 + http://sourceforge.net/project/showfiles.php?group_id=192439&package_id=256544
18.16 + http://blogtrader.net/dcaoyuan/category/NetBeans
18.17 + http://wiki.netbeans.org/Scala
18.18 +
18.19 +* jEdit 4.3 (final)
18.20 + http://www.jedit.org/
18.21 +
18.22 + Netbeans Project "jEdit": install official sources as ./contrib/jEdit/.
18.23 +
18.24 +* jEdit plugins:
18.25 + Netbeans Library "SideKick" = $HOME/.jedit/jars/SideKick.jar
18.26 + Netbeans Library "ErrorList" = $HOME/.jedit/jars/ErrorList.jar
18.27 + Netbeans Library "Hyperlinks" = $HOME/.jedit/jars/Hyperlinks.jar
18.28 +
18.29 +* Cobra Renderer 0.98.4
18.30 + http://lobobrowser.org/cobra.jsp
18.31 + Netbeans Library "Cobra-Renderer" = .../cobra.jar
18.32 + Netbenas Library "Rhino-JavaScript" = .../js.jar
18.33 +
18.34 +* Isabelle/Pure Scala components
18.35 + Netbeans Library "Isabelle-Pure" = ~~/lib/classes/Pure.jar
18.36 +
18.37 +
18.38 +Running the application within Netbeans
18.39 +=======================================
18.40 +
18.41 +* Project properties: add "Run" argument like
18.42 + -noserver -nobackground -settings=/home/makarius/isabelle/isabelle-jedit/dist
18.43 +
18.44 +* The Isabelle environment is obtained automatically via
18.45 + "$ISABELLE_HOME/bin/isabelle getenv", where ISABELLE_HOME is determined as follows:
18.46 +
18.47 + (1) via regular Isabelle settings,
18.48 + e.g. "isabelle env netbeans"
18.49 +
18.50 + (2) or via ISABELLE_HOME from raw process environment,
18.51 + e.g. "env ISABELLE_HOME=.../Isabelle netbeans"
18.52 +
18.53 + (3) or via JVM system properties (cf. "Run / VM Options")
18.54 + e.g. -Disabelle.home=.../Isabelle
18.55 +
18.56 +
18.57 +Misc notes
18.58 +==========
18.59 +
18.60 +- Netbeans config/Editors/Preferences/...-CustomPreferences.xml
18.61 +
18.62 + <entry javaType="java.lang.Integer" name="caret-blink-rate" xml:space="preserve">
18.63 + <value><![CDATA[0]]></value>
18.64 + </entry>
18.65 +
18.66 +-----------------------------------------------------------------------
18.67 +To run jedit with remote debugging enabled, I use the following
18.68 +command: "java
18.69 +-agentlib:jdwp=transport=dt_socket,suspend=y,server=y,address=XXXX
18.70 +-jar jedit.jar"
18.71 +
18.72 +where XXXX is any open port number you wish. The above invocation
18.73 +works for Sun's JDK 5.0. There's an alternate incantation for earlier
18.74 +releases. (See
18.75 +http://java.sun.com/j2se/1.5.0/docs/guide/jpda/conninv.html)
18.76 +-----------------------------------------------------------------------
19.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
19.2 +++ b/src/Tools/jEdit/build.xml Mon Jan 11 23:11:31 2010 +0100
19.3 @@ -0,0 +1,102 @@
19.4 +<?xml version="1.0" encoding="UTF-8"?>
19.5 +<!-- You may freely edit this file. See commented blocks below for -->
19.6 +<!-- some examples of how to customize the build. -->
19.7 +<!-- (If you delete it and reopen the project it will be recreated.) -->
19.8 +<project name="Isabelle-jEdit" default="default" basedir=".">
19.9 + <description>Builds, tests, and runs the project Isabelle-jEdit.</description>
19.10 + <import file="nbproject/build-impl.xml"/>
19.11 + <!--
19.12 +
19.13 + There exist several targets which are by default empty and which can be
19.14 + used for execution of your tasks. These targets are usually executed
19.15 + before and after some main targets. They are:
19.16 +
19.17 + -pre-init: called before initialization of project properties
19.18 + -post-init: called after initialization of project properties
19.19 + -pre-compile: called before javac compilation
19.20 + -post-compile: called after javac compilation
19.21 + -pre-compile-single: called before javac compilation of single file
19.22 + -post-compile-single: called after javac compilation of single file
19.23 + -pre-compile-test: called before javac compilation of JUnit tests
19.24 + -post-compile-test: called after javac compilation of JUnit tests
19.25 + -pre-compile-test-single: called before javac compilation of single JUnit test
19.26 + -post-compile-test-single: called after javac compilation of single JUunit test
19.27 + -pre-jar: called before JAR building
19.28 + -post-jar: called after JAR building
19.29 + -post-clean: called after cleaning build products
19.30 +
19.31 + (Targets beginning with '-' are not intended to be called on their own.)
19.32 +
19.33 + Example of inserting an obfuscator after compilation could look like this:
19.34 +
19.35 + <target name="-post-compile">
19.36 + <obfuscate>
19.37 + <fileset dir="${build.classes.dir}"/>
19.38 + </obfuscate>
19.39 + </target>
19.40 +
19.41 + For list of available properties check the imported
19.42 + nbproject/build-impl.xml file.
19.43 +
19.44 +
19.45 + Another way to customize the build is by overriding existing main targets.
19.46 + The targets of interest are:
19.47 +
19.48 + -init-macrodef-javac: defines macro for javac compilation
19.49 + -init-macrodef-junit: defines macro for junit execution
19.50 + -init-macrodef-debug: defines macro for class debugging
19.51 + -init-macrodef-java: defines macro for class execution
19.52 + -do-jar-with-manifest: JAR building (if you are using a manifest)
19.53 + -do-jar-without-manifest: JAR building (if you are not using a manifest)
19.54 + run: execution of project
19.55 + -javadoc-build: Javadoc generation
19.56 + test-report: JUnit report generation
19.57 +
19.58 + An example of overriding the target for project execution could look like this:
19.59 +
19.60 + <target name="run" depends="Isabelle-jEdit-impl.jar">
19.61 + <exec dir="bin" executable="launcher.exe">
19.62 + <arg file="${dist.jar}"/>
19.63 + </exec>
19.64 + </target>
19.65 +
19.66 + Notice that the overridden target depends on the jar target and not only on
19.67 + the compile target as the regular run target does. Again, for a list of available
19.68 + properties which you can use, check the target you are overriding in the
19.69 + nbproject/build-impl.xml file.
19.70 +
19.71 + -->
19.72 + <target name="run" depends="Isabelle-jEdit-impl.jar,Isabelle-jEdit-impl.run">
19.73 + </target>
19.74 + <target name="debug" depends="Isabelle-jEdit-impl.jar,Isabelle-jEdit-impl.debug">
19.75 + </target>
19.76 + <target name="-pre-jar">
19.77 + <copy file="plugin/services.xml" todir="${build.classes.dir}" />
19.78 + <copy file="plugin/dockables.xml" todir="${build.classes.dir}" />
19.79 + <copy file="plugin/actions.xml" todir="${build.classes.dir}" />
19.80 + <copy file="plugin/Isabelle.props" todir="${build.classes.dir}" />
19.81 + </target>
19.82 + <target name="-post-jar">
19.83 + <!-- jars -->
19.84 + <delete file="${dist.dir}/jars/lib/jEdit.jar" />
19.85 + <move todir="${dist.dir}/jars">
19.86 + <fileset dir="${dist.dir}/jars/lib" />
19.87 + </move>
19.88 + <copy file="${scala.library}" todir="${dist.dir}/jars" />
19.89 + <copy file="${scala.lib}/scala-swing.jar" todir="${dist.dir}/jars" />
19.90 + <!-- clean up -->
19.91 + <delete dir="{dist.dir}/jars/lib" />
19.92 + <!-- dist-template -->
19.93 + <copy file="dist-template/properties/jedit.props" tofile="${dist.dir}/properties" />
19.94 + <copy todir="${dist.dir}/modes">
19.95 + <fileset dir="dist-template/modes" />
19.96 + </copy>
19.97 + <copy todir="${dist.dir}/modes" overwrite="true">
19.98 + <fileset dir="${project.jEdit}/modes" />
19.99 + </copy>
19.100 + <replaceregexp byline="true" file="${dist.dir}/modes/catalog">
19.101 + <regexp pattern='(^.*NAME="javacc".*$)'/>
19.102 + <substitution expression="<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy"/>${line.separator}${line.separator}\1"/>
19.103 + </replaceregexp>
19.104 + </target>
19.105 +</project>
20.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
20.2 +++ b/src/Tools/jEdit/contrib/jEdit/build-nb.xml Mon Jan 11 23:11:31 2010 +0100
20.3 @@ -0,0 +1,41 @@
20.4 +<?xml version="1.0" encoding="UTF-8"?>
20.5 +<project name="jEdit">
20.6 + <import file="./build.xml"/>
20.7 + <property environment="env"/>
20.8 +
20.9 + <target name="run" depends="compile">
20.10 + <java classname="org.gjt.sp.jedit.jEdit" classpath="./build/jEdit.jar" dir="./" fork="true">
20.11 + <arg value="-noserver"/>
20.12 + <arg value="-nobackground"/>
20.13 + <arg value="-settings=${env.ISABELLE_HOME_USER}/jedit"/>
20.14 + </java>
20.15 + </target>
20.16 +
20.17 + <target name="debug-nb" depends="compile">
20.18 + <path id="cp" location="./build/jEdit.jar" />
20.19 +
20.20 + <nbjpdastart addressproperty="jpda.address" name="jEdit" transport="dt_socket">
20.21 + <classpath refid="cp"/>
20.22 + </nbjpdastart>
20.23 +
20.24 + <java classname="org.gjt.sp.jedit.jEdit" classpathref="cp" fork="true" dir="./">
20.25 + <jvmarg value="-Xdebug"/>
20.26 + <jvmarg value="-Xrunjdwp:transport=dt_socket,address=${jpda.address}"/>
20.27 + </java>
20.28 + </target>
20.29 +
20.30 + <target name="profile-nb" depends="compile">
20.31 + <fail unless="netbeans.home">This target can only run inside the NetBeans IDE.</fail>
20.32 +
20.33 + <path id="cp" location="./build/jEdit.jar" />
20.34 +
20.35 + <nbprofiledirect>
20.36 + <classpath refid="cp"/>
20.37 + </nbprofiledirect>
20.38 +
20.39 + <java classname="org.gjt.sp.jedit.jEdit" fork="true" logError="yes" dir="." classpathref="cp">
20.40 + <classpath refid="cp"/>
20.41 + <jvmarg value="${profiler.info.jvmargs.agent}"/>
20.42 + </java>
20.43 + </target>
20.44 +</project>
20.45 \ No newline at end of file
21.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
21.2 +++ b/src/Tools/jEdit/contrib/jEdit/nbproject/project.xml Mon Jan 11 23:11:31 2010 +0100
21.3 @@ -0,0 +1,118 @@
21.4 +<?xml version="1.0" encoding="UTF-8"?>
21.5 +<project xmlns="http://www.netbeans.org/ns/project/1">
21.6 + <type>org.netbeans.modules.ant.freeform</type>
21.7 + <configuration>
21.8 + <general-data xmlns="http://www.netbeans.org/ns/freeform-project/1">
21.9 + <name>jEdit</name>
21.10 + </general-data>
21.11 + <general-data xmlns="http://www.netbeans.org/ns/freeform-project/2">
21.12 + <!-- Do not use Project Properties customizer when editing this file manually. -->
21.13 + <name>jEdit</name>
21.14 + <properties>
21.15 + <property name="ant.script">build-nb.xml</property>
21.16 + </properties>
21.17 + <folders>
21.18 + <source-folder>
21.19 + <label>jEdit</label>
21.20 + <location>.</location>
21.21 + <encoding>UTF-8</encoding>
21.22 + </source-folder>
21.23 + <source-folder>
21.24 + <label>Source Packages</label>
21.25 + <type>java</type>
21.26 + <location>.</location>
21.27 + <excludes>build/** doc/** icons/** macros/** modes/** package-files/**</excludes>
21.28 + <encoding>UTF-8</encoding>
21.29 + </source-folder>
21.30 + </folders>
21.31 + <ide-actions>
21.32 + <action name="build">
21.33 + <script>${ant.script}</script>
21.34 + <target>build</target>
21.35 + </action>
21.36 + <action name="clean">
21.37 + <script>${ant.script}</script>
21.38 + <target>clean</target>
21.39 + </action>
21.40 + <action name="javadoc">
21.41 + <script>${ant.script}</script>
21.42 + <target>docs-javadoc</target>
21.43 + </action>
21.44 + <action name="run">
21.45 + <script>${ant.script}</script>
21.46 + <target>run</target>
21.47 + </action>
21.48 + <action name="rebuild">
21.49 + <script>${ant.script}</script>
21.50 + <target>clean</target>
21.51 + <target>build</target>
21.52 + </action>
21.53 + <action name="debug">
21.54 + <script>build-nb.xml</script>
21.55 + <target>debug-nb</target>
21.56 + </action>
21.57 + </ide-actions>
21.58 + <export>
21.59 + <type>jar</type>
21.60 + <location>build/jEdit.jar</location>
21.61 + <script>${ant.script}</script>
21.62 + <build-target>build</build-target>
21.63 + </export>
21.64 + <view>
21.65 + <items>
21.66 + <source-folder style="packages">
21.67 + <label>Source Packages</label>
21.68 + <location>.</location>
21.69 + <excludes>build/** doc/** icons/** macros/** modes/** package-files/**</excludes>
21.70 + </source-folder>
21.71 + <source-file>
21.72 + <location>${ant.script}</location>
21.73 + </source-file>
21.74 + </items>
21.75 + <context-menu>
21.76 + <ide-action name="build"/>
21.77 + <ide-action name="rebuild"/>
21.78 + <ide-action name="clean"/>
21.79 + <ide-action name="javadoc"/>
21.80 + <ide-action name="run"/>
21.81 + <ide-action name="debug"/>
21.82 + </context-menu>
21.83 + </view>
21.84 + <subprojects/>
21.85 + </general-data>
21.86 + <java-data xmlns="http://www.netbeans.org/ns/freeform-project-java/1">
21.87 + <compilation-unit>
21.88 + <package-root>.</package-root>
21.89 + <classpath mode="compile">.</classpath>
21.90 + <built-to>build/jEdit.jar</built-to>
21.91 + <source-level>1.5</source-level>
21.92 + </compilation-unit>
21.93 + </java-data>
21.94 + <preferences xmlns="http://www.netbeans.org/ns/auxiliary-configuration-preferences/1">
21.95 + <module name="org-netbeans-modules-editor-indent">
21.96 + <node name="CodeStyle">
21.97 + <property name="usedProfile" value="default"/>
21.98 + <node name="project">
21.99 + <property name="spaces-per-tab" value="2"/>
21.100 + <property name="tab-size" value="2"/>
21.101 + <property name="indent-shift-width" value="2"/>
21.102 + <property name="text-limit-width" value="100"/>
21.103 + <property name="expand-tabs" value="true"/>
21.104 + </node>
21.105 + </node>
21.106 + <node name="text">
21.107 + <node name="x-java">
21.108 + <node name="CodeStyle">
21.109 + <node name="project">
21.110 + <property name="tab-size" value="4"/>
21.111 + <property name="text-limit-width" value="100"/>
21.112 + <property name="spaces-per-tab" value="2"/>
21.113 + <property name="indent-shift-width" value="2"/>
21.114 + </node>
21.115 + </node>
21.116 + </node>
21.117 + </node>
21.118 + </module>
21.119 + </preferences>
21.120 + </configuration>
21.121 +</project>
22.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
22.2 +++ b/src/Tools/jEdit/dist-template/etc/settings Mon Jan 11 23:11:31 2010 +0100
22.3 @@ -0,0 +1,9 @@
22.4 +JEDIT_HOME="$COMPONENT"
22.5 +
22.6 +JEDIT_JAVA_OPTIONS="-Xms128m -Xmx512m -Xss2m"
22.7 +#JEDIT_JAVA_OPTIONS="-server -Xms128m -Xmx1024m -Xss4m"
22.8 +JEDIT_OPTIONS="-reuseview -noserver -nobackground"
22.9 +
22.10 +ISABELLE_JEDIT_OPTIONS="-m xsymbols -m no_brackets -m no_type_brackets"
22.11 +
22.12 +ISABELLE_TOOLS="$ISABELLE_TOOLS:$JEDIT_HOME/lib/Tools"
23.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
23.2 +++ b/src/Tools/jEdit/dist-template/lib/Tools/jedit Mon Jan 11 23:11:31 2010 +0100
23.3 @@ -0,0 +1,117 @@
23.4 +#!/usr/bin/env bash
23.5 +#
23.6 +# Author: Makarius
23.7 +#
23.8 +# DESCRIPTION: Isabelle/jEdit interface wrapper
23.9 +
23.10 +
23.11 +## diagnostics
23.12 +
23.13 +PRG="$(basename "$0")"
23.14 +
23.15 +usage()
23.16 +{
23.17 + echo
23.18 + echo "Usage: isabelle $PRG [OPTIONS] [FILES ...]"
23.19 + echo
23.20 + echo " Options are:"
23.21 + echo " -J OPTION add JVM runtime option"
23.22 + echo " (default JEDIT_JAVA_OPTIONS=$JEDIT_JAVA_OPTIONS)"
23.23 + echo " -d enable debugger"
23.24 + echo " -j OPTION add jEdit runtime option"
23.25 + echo " (default JEDIT_OPTIONS=$JEDIT_OPTIONS)"
23.26 + echo " -l NAME logic image name (default ISABELLE_LOGIC=$ISABELLE_LOGIC)"
23.27 + echo " -m MODE add print mode for output"
23.28 + echo
23.29 + echo "Start jEdit with Isabelle plugin setup and opens theory FILES"
23.30 + echo "(default ~/Scratch.thy)."
23.31 + echo
23.32 + exit 1
23.33 +}
23.34 +
23.35 +fail()
23.36 +{
23.37 + echo "$1" >&2
23.38 + exit 2
23.39 +}
23.40 +
23.41 +
23.42 +## process command line
23.43 +
23.44 +# options
23.45 +
23.46 +JEDIT_LOGIC="$ISABELLE_LOGIC"
23.47 +JEDIT_PRINT_MODE=""
23.48 +
23.49 +getoptions()
23.50 +{
23.51 + OPTIND=1
23.52 + while getopts "J:dj:l:m:" OPT
23.53 + do
23.54 + case "$OPT" in
23.55 + J)
23.56 + JAVA_ARGS["${#JAVA_ARGS[@]}"]="$OPTARG"
23.57 + ;;
23.58 + d)
23.59 + JAVA_ARGS["${#JAVA_ARGS[@]}"]="-Xdebug"
23.60 + JAVA_ARGS["${#JAVA_ARGS[@]}"]="-Xrunjdwp:transport=dt_socket,server=y,suspend=n"
23.61 + ;;
23.62 + j)
23.63 + ARGS["${#ARGS[@]}"]="$OPTARG"
23.64 + ;;
23.65 + l)
23.66 + JEDIT_LOGIC="$OPTARG"
23.67 + ;;
23.68 + m)
23.69 + if [ -z "$JEDIT_PRINT_MODE" ]; then
23.70 + JEDIT_PRINT_MODE="$OPTARG"
23.71 + else
23.72 + JEDIT_PRINT_MODE="$JEDIT_PRINT_MODE,$OPTARG"
23.73 + fi
23.74 + ;;
23.75 + \?)
23.76 + usage
23.77 + ;;
23.78 + esac
23.79 + done
23.80 +}
23.81 +
23.82 +declare -a JAVA_ARGS; eval "JAVA_ARGS=($JEDIT_JAVA_OPTIONS)"
23.83 +[ -n "$SCALA_HOME" ] && JAVA_ARGS["${#JAVA_ARGS[@]}"]="-Dscala.home=$SCALA_HOME"
23.84 +
23.85 +declare -a ARGS; eval "ARGS=($JEDIT_OPTIONS)"
23.86 +
23.87 +declare -a OPTIONS; eval "OPTIONS=($ISABELLE_JEDIT_OPTIONS)"
23.88 +getoptions "${OPTIONS[@]}"
23.89 +
23.90 +getoptions "$@"
23.91 +shift $(($OPTIND - 1))
23.92 +
23.93 +
23.94 +# args
23.95 +
23.96 +if [ "$#" -eq 0 ]; then
23.97 + ARGS["${#ARGS[@]}"]="Scratch.thy"
23.98 +else
23.99 + while [ "$#" -gt 0 ]; do
23.100 + ARGS["${#ARGS[@]}"]="$(jvmpath "$1")"
23.101 + shift
23.102 + done
23.103 +fi
23.104 +
23.105 +
23.106 +## main
23.107 +
23.108 +case "$JEDIT_LOGIC" in
23.109 + /*)
23.110 + ;;
23.111 + */*)
23.112 + JEDIT_LOGIC="$(pwd -P)/$JEDIT_LOGIC"
23.113 + ;;
23.114 +esac
23.115 +
23.116 +export JEDIT_LOGIC JEDIT_PRINT_MODE
23.117 +
23.118 +exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" \
23.119 + -jar "$(jvmpath "$JEDIT_HOME/jedit.jar")" \
23.120 + "-settings=$(jvmpath "$ISABELLE_HOME_USER/jedit")" "${ARGS[@]}"
24.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
24.2 +++ b/src/Tools/jEdit/dist-template/modes/isabelle-session.xml Mon Jan 11 23:11:31 2010 +0100
24.3 @@ -0,0 +1,41 @@
24.4 +<?xml version="1.0"?>
24.5 +<!DOCTYPE MODE SYSTEM "xmode.dtd">
24.6 +
24.7 +<!-- Isabelle session mode -->
24.8 +<MODE>
24.9 + <PROPS>
24.10 + <PROPERTY NAME="commentStart" VALUE="(*"/>
24.11 + <PROPERTY NAME="commentEnd" VALUE="*)"/>
24.12 + <PROPERTY NAME="noWordSep" VALUE="_'.?"/>
24.13 + <PROPERTY NAME="unalignedOpenBrackets" VALUE="(" />
24.14 + <PROPERTY NAME="unalignedCloseBrackets" VALUE=")" />
24.15 + <PROPERTY NAME="tabSize" VALUE="2" />
24.16 + <PROPERTY NAME="indentSize" VALUE="2" />
24.17 + </PROPS>
24.18 + <RULES IGNORE_CASE="FALSE" HIGHLIGHT_DIGITS="FALSE" ESCAPE="\">
24.19 + <SPAN TYPE="COMMENT1">
24.20 + <BEGIN>(*</BEGIN>
24.21 + <END>*)</END>
24.22 + </SPAN>
24.23 + <SPAN TYPE="COMMENT3">
24.24 + <BEGIN>{*</BEGIN>
24.25 + <END>*}</END>
24.26 + </SPAN>
24.27 + <SPAN TYPE="LITERAL1">
24.28 + <BEGIN>`</BEGIN>
24.29 + <END>`</END>
24.30 + </SPAN>
24.31 + <SPAN TYPE="LITERAL3">
24.32 + <BEGIN>"</BEGIN>
24.33 + <END>"</END>
24.34 + </SPAN>
24.35 + <KEYWORDS>
24.36 + <KEYWORD1>session</KEYWORD1>
24.37 + <KEYWORD2>parent</KEYWORD2>
24.38 + <KEYWORD2>imports</KEYWORD2>
24.39 + <KEYWORD2>uses</KEYWORD2>
24.40 + <KEYWORD2>options</KEYWORD2>
24.41 + <KEYWORD2>dependencies</KEYWORD2>
24.42 + </KEYWORDS>
24.43 + </RULES>
24.44 +</MODE>
25.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
25.2 +++ b/src/Tools/jEdit/dist-template/modes/isabelle.xml Mon Jan 11 23:11:31 2010 +0100
25.3 @@ -0,0 +1,43 @@
25.4 +<?xml version="1.0"?>
25.5 +<!DOCTYPE MODE SYSTEM "xmode.dtd">
25.6 +
25.7 +<!-- Isabelle theory mode -->
25.8 +<MODE>
25.9 + <PROPS>
25.10 + <PROPERTY NAME="commentStart" VALUE="(*"/>
25.11 + <PROPERTY NAME="commentEnd" VALUE="*)"/>
25.12 + <PROPERTY NAME="noWordSep" VALUE="_'.?"/>
25.13 + <PROPERTY NAME="indentOpenBrackets" VALUE="{"/>
25.14 + <PROPERTY NAME="indentCloseBrackets" VALUE="}"/>
25.15 + <PROPERTY NAME="unalignedOpenBrackets" VALUE="(" />
25.16 + <PROPERTY NAME="unalignedCloseBrackets" VALUE=")" />
25.17 + <PROPERTY NAME="tabSize" VALUE="2" />
25.18 + <PROPERTY NAME="indentSize" VALUE="2" />
25.19 + </PROPS>
25.20 + <RULES IGNORE_CASE="FALSE" HIGHLIGHT_DIGITS="FALSE" ESCAPE="\">
25.21 + <SPAN TYPE="COMMENT1">
25.22 + <BEGIN>(*</BEGIN>
25.23 + <END>*)</END>
25.24 + </SPAN>
25.25 + <SPAN TYPE="COMMENT3">
25.26 + <BEGIN>{*</BEGIN>
25.27 + <END>*}</END>
25.28 + </SPAN>
25.29 + <SPAN TYPE="LITERAL1">
25.30 + <BEGIN>`</BEGIN>
25.31 + <END>`</END>
25.32 + </SPAN>
25.33 + <SPAN TYPE="LITERAL3">
25.34 + <BEGIN>"</BEGIN>
25.35 + <END>"</END>
25.36 + </SPAN>
25.37 + <KEYWORDS>
25.38 + <KEYWORD2>header</KEYWORD2>
25.39 + <KEYWORD1>theory</KEYWORD1>
25.40 + <KEYWORD2>imports</KEYWORD2>
25.41 + <KEYWORD2>uses</KEYWORD2>
25.42 + <KEYWORD2>begin</KEYWORD2>
25.43 + <KEYWORD2>end</KEYWORD2>
25.44 + </KEYWORDS>
25.45 + </RULES>
25.46 +</MODE>
26.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
26.2 +++ b/src/Tools/jEdit/dist-template/properties/jedit.props Mon Jan 11 23:11:31 2010 +0100
26.3 @@ -0,0 +1,191 @@
26.4 +#jEdit properties
26.5 +buffer.deepIndent=false
26.6 +buffer.encoding=UTF-8-Isabelle
26.7 +buffer.indentSize=2
26.8 +buffer.lineSeparator=\n
26.9 +buffer.maxLineLen=100
26.10 +buffer.noTabs=true
26.11 +buffer.sidekick.keystroke-parse=true
26.12 +buffer.tabSize=2
26.13 +delete-line.shortcut=A+d
26.14 +delete.shortcut2=C+d
26.15 +encoding.opt-out.Big5-HKSCS=true
26.16 +encoding.opt-out.Big5=true
26.17 +encoding.opt-out.COMPOUND_TEXT=true
26.18 +encoding.opt-out.EUC-JP=true
26.19 +encoding.opt-out.EUC-KR=true
26.20 +encoding.opt-out.GB18030=true
26.21 +encoding.opt-out.GB2312=true
26.22 +encoding.opt-out.GBK=true
26.23 +encoding.opt-out.IBM-Thai=true
26.24 +encoding.opt-out.IBM00858=true
26.25 +encoding.opt-out.IBM01140=true
26.26 +encoding.opt-out.IBM01141=true
26.27 +encoding.opt-out.IBM01142=true
26.28 +encoding.opt-out.IBM01143=true
26.29 +encoding.opt-out.IBM01144=true
26.30 +encoding.opt-out.IBM01145=true
26.31 +encoding.opt-out.IBM01146=true
26.32 +encoding.opt-out.IBM01147=true
26.33 +encoding.opt-out.IBM01148=true
26.34 +encoding.opt-out.IBM01149=true
26.35 +encoding.opt-out.IBM037=true
26.36 +encoding.opt-out.IBM1026=true
26.37 +encoding.opt-out.IBM1047=true
26.38 +encoding.opt-out.IBM273=true
26.39 +encoding.opt-out.IBM277=true
26.40 +encoding.opt-out.IBM278=true
26.41 +encoding.opt-out.IBM280=true
26.42 +encoding.opt-out.IBM284=true
26.43 +encoding.opt-out.IBM285=true
26.44 +encoding.opt-out.IBM297=true
26.45 +encoding.opt-out.IBM420=true
26.46 +encoding.opt-out.IBM424=true
26.47 +encoding.opt-out.IBM437=true
26.48 +encoding.opt-out.IBM500=true
26.49 +encoding.opt-out.IBM775=true
26.50 +encoding.opt-out.IBM850=true
26.51 +encoding.opt-out.IBM852=true
26.52 +encoding.opt-out.IBM855=true
26.53 +encoding.opt-out.IBM857=true
26.54 +encoding.opt-out.IBM860=true
26.55 +encoding.opt-out.IBM861=true
26.56 +encoding.opt-out.IBM862=true
26.57 +encoding.opt-out.IBM863=true
26.58 +encoding.opt-out.IBM864=true
26.59 +encoding.opt-out.IBM865=true
26.60 +encoding.opt-out.IBM866=true
26.61 +encoding.opt-out.IBM868=true
26.62 +encoding.opt-out.IBM869=true
26.63 +encoding.opt-out.IBM870=true
26.64 +encoding.opt-out.IBM871=true
26.65 +encoding.opt-out.IBM918=true
26.66 +encoding.opt-out.ISO-2022-CN=true
26.67 +encoding.opt-out.ISO-2022-JP-2=true
26.68 +encoding.opt-out.ISO-2022-JP=true
26.69 +encoding.opt-out.ISO-2022-KR=true
26.70 +encoding.opt-out.ISO-8859-13=true
26.71 +encoding.opt-out.ISO-8859-2=true
26.72 +encoding.opt-out.ISO-8859-3=true
26.73 +encoding.opt-out.ISO-8859-4=true
26.74 +encoding.opt-out.ISO-8859-5=true
26.75 +encoding.opt-out.ISO-8859-6=true
26.76 +encoding.opt-out.ISO-8859-7=true
26.77 +encoding.opt-out.ISO-8859-8=true
26.78 +encoding.opt-out.ISO-8859-9=true
26.79 +encoding.opt-out.JIS_X0201=true
26.80 +encoding.opt-out.JIS_X0212-1990=true
26.81 +encoding.opt-out.KOI8-R=true
26.82 +encoding.opt-out.KOI8-U=true
26.83 +encoding.opt-out.Shift_JIS=true
26.84 +encoding.opt-out.TIS-620=true
26.85 +encoding.opt-out.UTF-16=true
26.86 +encoding.opt-out.UTF-16BE=true
26.87 +encoding.opt-out.UTF-16LE=true
26.88 +encoding.opt-out.UTF-32=true
26.89 +encoding.opt-out.UTF-32BE=true
26.90 +encoding.opt-out.UTF-32LE=true
26.91 +encoding.opt-out.X-UTF-32BE-BOM=true
26.92 +encoding.opt-out.X-UTF-32LE-BOM=true
26.93 +encoding.opt-out.windows-1250=true
26.94 +encoding.opt-out.windows-1251=true
26.95 +encoding.opt-out.windows-1253=true
26.96 +encoding.opt-out.windows-1254=true
26.97 +encoding.opt-out.windows-1255=true
26.98 +encoding.opt-out.windows-1256=true
26.99 +encoding.opt-out.windows-1257=true
26.100 +encoding.opt-out.windows-1258=true
26.101 +encoding.opt-out.windows-31j=true
26.102 +encoding.opt-out.x-Big5-Solaris=true
26.103 +encoding.opt-out.x-EUC-TW=true
26.104 +encoding.opt-out.x-IBM1006=true
26.105 +encoding.opt-out.x-IBM1025=true
26.106 +encoding.opt-out.x-IBM1046=true
26.107 +encoding.opt-out.x-IBM1097=true
26.108 +encoding.opt-out.x-IBM1098=true
26.109 +encoding.opt-out.x-IBM1112=true
26.110 +encoding.opt-out.x-IBM1122=true
26.111 +encoding.opt-out.x-IBM1123=true
26.112 +encoding.opt-out.x-IBM1124=true
26.113 +encoding.opt-out.x-IBM1381=true
26.114 +encoding.opt-out.x-IBM1383=true
26.115 +encoding.opt-out.x-IBM33722=true
26.116 +encoding.opt-out.x-IBM737=true
26.117 +encoding.opt-out.x-IBM834=true
26.118 +encoding.opt-out.x-IBM856=true
26.119 +encoding.opt-out.x-IBM874=true
26.120 +encoding.opt-out.x-IBM875=true
26.121 +encoding.opt-out.x-IBM921=true
26.122 +encoding.opt-out.x-IBM922=true
26.123 +encoding.opt-out.x-IBM930=true
26.124 +encoding.opt-out.x-IBM933=true
26.125 +encoding.opt-out.x-IBM935=true
26.126 +encoding.opt-out.x-IBM937=true
26.127 +encoding.opt-out.x-IBM939=true
26.128 +encoding.opt-out.x-IBM942=true
26.129 +encoding.opt-out.x-IBM942C=true
26.130 +encoding.opt-out.x-IBM943=true
26.131 +encoding.opt-out.x-IBM943C=true
26.132 +encoding.opt-out.x-IBM948=true
26.133 +encoding.opt-out.x-IBM949=true
26.134 +encoding.opt-out.x-IBM949C=true
26.135 +encoding.opt-out.x-IBM950=true
26.136 +encoding.opt-out.x-IBM964=true
26.137 +encoding.opt-out.x-IBM970=true
26.138 +encoding.opt-out.x-ISCII91=true
26.139 +encoding.opt-out.x-ISO-2022-CN-CNS=true
26.140 +encoding.opt-out.x-ISO-2022-CN-GB=true
26.141 +encoding.opt-out.x-JIS0208=true
26.142 +encoding.opt-out.x-JISAutoDetect=true
26.143 +encoding.opt-out.x-Johab=true
26.144 +encoding.opt-out.x-MS932_0213=true
26.145 +encoding.opt-out.x-MS950-HKSCS=true
26.146 +encoding.opt-out.x-MacArabic=true
26.147 +encoding.opt-out.x-MacCentralEurope=true
26.148 +encoding.opt-out.x-MacCroatian=true
26.149 +encoding.opt-out.x-MacCyrillic=true
26.150 +encoding.opt-out.x-MacDingbat=true
26.151 +encoding.opt-out.x-MacGreek=true
26.152 +encoding.opt-out.x-MacHebrew=true
26.153 +encoding.opt-out.x-MacIceland=true
26.154 +encoding.opt-out.x-MacRoman=true
26.155 +encoding.opt-out.x-MacRomania=true
26.156 +encoding.opt-out.x-MacSymbol=true
26.157 +encoding.opt-out.x-MacThai=true
26.158 +encoding.opt-out.x-MacTurkish=true
26.159 +encoding.opt-out.x-MacUkraine=true
26.160 +encoding.opt-out.x-PCK=true
26.161 +encoding.opt-out.x-SJIS_0213=true
26.162 +encoding.opt-out.x-UTF-16LE-BOM=true
26.163 +encoding.opt-out.x-euc-jp-linux=true
26.164 +encoding.opt-out.x-eucJP-Open=true
26.165 +encoding.opt-out.x-iso-8859-11=true
26.166 +encoding.opt-out.x-mswin-936=true
26.167 +encoding.opt-out.x-windows-50220=true
26.168 +encoding.opt-out.x-windows-50221=true
26.169 +encoding.opt-out.x-windows-874=true
26.170 +encoding.opt-out.x-windows-949=true
26.171 +encoding.opt-out.x-windows-950=true
26.172 +encoding.opt-out.x-windows-iso2022jp=true
26.173 +encodingDetectors=BOM XML-PI buffer-local-property
26.174 +fallbackEncodings=UTF-8 ISO-8859-15 US-ASCII
26.175 +firstTime=false
26.176 +isabelle-protocol.dock-position=bottom
26.177 +isabelle-results.dock-position=bottom
26.178 +isabelle.activate.shortcut=CS+ENTER
26.179 +mode.isabelle.sidekick.showStatusWindow.label=true
26.180 +sidekick-tree.dock-position=right
26.181 +sidekick.buffer-save-parse=true
26.182 +sidekick.complete-delay=300
26.183 +tip.show=false
26.184 +view.antiAlias=standard
26.185 +view.blockCaret=true
26.186 +view.caretBlink=false
26.187 +view.eolMarkers=false
26.188 +view.extendedState=0
26.189 +view.font=IsabelleText
26.190 +view.fontsize=18
26.191 +view.fracFontMetrics=false
26.192 +view.gutter.fontsize=12
26.193 +view.middleMousePaste=true
26.194 +view.showToolbar=false
27.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
27.2 +++ b/src/Tools/jEdit/makedist Mon Jan 11 23:11:31 2010 +0100
27.3 @@ -0,0 +1,98 @@
27.4 +#!/usr/bin/env bash
27.5 +#
27.6 +# makedist -- make Isabelle/jEdit distribution
27.7 +
27.8 +## self references
27.9 +
27.10 +PRG=$(basename "$0")
27.11 +THIS=$(cd "$(dirname "$0")"; pwd)
27.12 +SUPER=$(cd "$THIS/.."; pwd)
27.13 +
27.14 +
27.15 +## diagnostics
27.16 +
27.17 +JEDIT_HOME="/home/isajedit/jedit-orig/4.3pre17"
27.18 +
27.19 +function usage()
27.20 +{
27.21 + echo
27.22 + echo "Usage: $PRG [OPTIONS]"
27.23 + echo
27.24 + echo " Options are:"
27.25 + echo " -j DIR specify original jEdit distribution"
27.26 + echo " (default: $JEDIT_HOME)"
27.27 + echo
27.28 + echo " Produce Isabelle/jEdit distribution from Netbeans build"
27.29 + echo " in $THIS/dist"
27.30 + echo
27.31 + exit 1
27.32 +}
27.33 +
27.34 +fail()
27.35 +{
27.36 + echo "$1" >&2
27.37 + exit 2
27.38 +}
27.39 +
27.40 +
27.41 +## process command line
27.42 +
27.43 +# options
27.44 +
27.45 +while getopts "j:s:" OPT
27.46 +do
27.47 + case "$OPT" in
27.48 + j)
27.49 + JEDIT_HOME="$OPTARG"
27.50 + ;;
27.51 + \?)
27.52 + usage
27.53 + ;;
27.54 + esac
27.55 +done
27.56 +
27.57 +shift $(($OPTIND - 1))
27.58 +
27.59 +
27.60 +# args
27.61 +
27.62 +[ "$#" -ne 0 ] && usage
27.63 +
27.64 +
27.65 +## main
27.66 +
27.67 +cd "$THIS/dist" || fail "Bad directory: $THIS/dist"
27.68 +
27.69 +
27.70 +# target name
27.71 +
27.72 +VERSION=$(basename "$JEDIT_HOME")
27.73 +JEDIT="jedit-${VERSION}"
27.74 +
27.75 +rm -rf "$JEDIT" jedit
27.76 +mkdir "$JEDIT"
27.77 +ln -s "$JEDIT" jedit
27.78 +
27.79 +
27.80 +# copy stuff
27.81 +
27.82 +[ "$JEDIT_HOME/jedit.jar" ] || fail "Bad original jEdit directory: $JEDIT_HOME"
27.83 +cp -R "$JEDIT_HOME/." "$JEDIT/."
27.84 +rm -rf "$JEDIT/jEdit" "$JEDIT/build-support"
27.85 +
27.86 +mkdir -p "$JEDIT/jars"
27.87 +cp -R jars/. "$JEDIT/jars/."
27.88 +
27.89 +cp -R "$THIS/dist-template/." "$JEDIT/."
27.90 +
27.91 +perl -i -e 'while (<>) { if (m/NAME="javacc"/) {
27.92 + print qq,<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy"/>\n\n,;
27.93 + print qq,<MODE NAME="isabelle-session" FILE="isabelle-session.xml" FILE_NAME_GLOB="session.root"/>\n\n,; }
27.94 + print; }' "$JEDIT/modes/catalog"
27.95 +
27.96 +
27.97 +# build archive
27.98 +
27.99 +echo "${JEDIT}.tar.gz"
27.100 +tar czf "${JEDIT}.tar.gz" "$JEDIT" jedit
27.101 +ln -sf "${JEDIT}.tar.gz" jedit.tar.gz
28.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
28.2 +++ b/src/Tools/jEdit/manifest.mf Mon Jan 11 23:11:31 2010 +0100
28.3 @@ -0,0 +1,3 @@
28.4 +Manifest-Version: 1.0
28.5 +X-COMMENT: Main-Class will be added automatically by build
28.6 +
29.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
29.2 +++ b/src/Tools/jEdit/nbproject/build-impl.xml Mon Jan 11 23:11:31 2010 +0100
29.3 @@ -0,0 +1,709 @@
29.4 +<?xml version="1.0" encoding="UTF-8"?>
29.5 +<!--
29.6 +*** GENERATED FROM project.xml - DO NOT EDIT ***
29.7 +*** EDIT ../build.xml INSTEAD ***
29.8 +
29.9 +For the purpose of easier reading the script
29.10 +is divided into following sections:
29.11 +
29.12 + - initialization
29.13 + - compilation
29.14 + - jar
29.15 + - execution
29.16 + - debugging
29.17 + - javadoc
29.18 + - junit compilation
29.19 + - junit execution
29.20 + - junit debugging
29.21 + - applet
29.22 + - cleanup
29.23 +
29.24 +
29.25 + -->
29.26 +<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">
29.27 + <target depends="test,jar,javadoc" description="Build and test whole project." name="default"/>
29.28 + <!--
29.29 + ======================
29.30 + INITIALIZATION SECTION
29.31 + ======================
29.32 + -->
29.33 + <target name="-pre-init">
29.34 + <!-- Empty placeholder for easier customization. -->
29.35 + <!-- You can override this target in the ../build.xml file. -->
29.36 + </target>
29.37 + <target depends="-pre-init" name="-init-private">
29.38 + <property file="nbproject/private/config.properties"/>
29.39 + <property file="nbproject/private/configs/${config}.properties"/>
29.40 + <property file="nbproject/private/private.properties"/>
29.41 + <property environment="env"/>
29.42 + <condition property="scala.home" value="${env.SCALA_HOME}">
29.43 + <isset property="env.SCALA_HOME"/>
29.44 + </condition>
29.45 + <fail unless="scala.home">
29.46 +You must set SCALA_HOME or environment property and append "-J-Dscala.home=scalahomepath"
29.47 +property to the end of "netbeans_default_options" in NetBeansInstallationPath/etc/netbeans.conf to point to
29.48 +Scala installation directory.
29.49 + </fail>
29.50 + <property name="scala.compiler" value="${scala.home}/lib/scala-compiler.jar"/>
29.51 + <property name="scala.library" value="${scala.home}/lib/scala-library.jar"/>
29.52 + <property name="scala.lib" value="${scala.home}/lib"/>
29.53 + <taskdef resource="scala/tools/ant/antlib.xml">
29.54 + <classpath>
29.55 + <pathelement location="${scala.compiler}"/>
29.56 + <pathelement location="${scala.library}"/>
29.57 + </classpath>
29.58 + </taskdef>
29.59 + <chmod dir="${scala.home}/bin" includes="**/*" perm="u+rx"/>
29.60 + </target>
29.61 + <target depends="-pre-init,-init-private" name="-init-user">
29.62 + <property file="${user.properties.file}"/>
29.63 + <!-- The two properties below are usually overridden -->
29.64 + <!-- by the active platform. Just a fallback. -->
29.65 + <property name="default.javac.source" value="1.4"/>
29.66 + <property name="default.javac.target" value="1.4"/>
29.67 + </target>
29.68 + <target depends="-pre-init,-init-private,-init-user" name="-init-project">
29.69 + <property file="nbproject/configs/${config}.properties"/>
29.70 + <property file="nbproject/project.properties"/>
29.71 + </target>
29.72 + <target depends="-pre-init,-init-private,-init-user,-init-project,-init-macrodef-property" name="-do-init">
29.73 + <available file="${manifest.file}" property="manifest.available"/>
29.74 + <condition property="manifest.available+main.class">
29.75 + <and>
29.76 + <isset property="manifest.available"/>
29.77 + <isset property="main.class"/>
29.78 + <not>
29.79 + <equals arg1="${main.class}" arg2="" trim="true"/>
29.80 + </not>
29.81 + </and>
29.82 + </condition>
29.83 + <condition property="manifest.available+main.class+mkdist.available">
29.84 + <and>
29.85 + <istrue value="${manifest.available+main.class}"/>
29.86 + <isset property="libs.CopyLibs.classpath"/>
29.87 + </and>
29.88 + </condition>
29.89 + <condition property="have.tests">
29.90 + <or/>
29.91 + </condition>
29.92 + <condition property="have.sources">
29.93 + <or>
29.94 + <available file="${src.dir}"/>
29.95 + </or>
29.96 + </condition>
29.97 + <condition property="netbeans.home+have.tests">
29.98 + <and>
29.99 + <isset property="netbeans.home"/>
29.100 + <isset property="have.tests"/>
29.101 + </and>
29.102 + </condition>
29.103 + <condition property="no.javadoc.preview">
29.104 + <and>
29.105 + <isset property="javadoc.preview"/>
29.106 + <isfalse value="${javadoc.preview}"/>
29.107 + </and>
29.108 + </condition>
29.109 + <property name="run.jvmargs" value=""/>
29.110 + <property name="javac.compilerargs" value=""/>
29.111 + <property name="work.dir" value="${basedir}"/>
29.112 + <condition property="no.deps">
29.113 + <and>
29.114 + <istrue value="${no.dependencies}"/>
29.115 + </and>
29.116 + </condition>
29.117 + <property name="javac.debug" value="true"/>
29.118 + <property name="javadoc.preview" value="true"/>
29.119 + <property name="application.args" value=""/>
29.120 + <property name="source.encoding" value="${file.encoding}"/>
29.121 + <condition property="javadoc.encoding.used" value="${javadoc.encoding}">
29.122 + <and>
29.123 + <isset property="javadoc.encoding"/>
29.124 + <not>
29.125 + <equals arg1="${javadoc.encoding}" arg2=""/>
29.126 + </not>
29.127 + </and>
29.128 + </condition>
29.129 + <property name="javadoc.encoding.used" value="${source.encoding}"/>
29.130 + <property name="includes" value="**"/>
29.131 + <property name="excludes" value=""/>
29.132 + <property name="do.depend" value="false"/>
29.133 + <condition property="do.depend.true">
29.134 + <istrue value="${do.depend}"/>
29.135 + </condition>
29.136 + <condition else="" property="javac.compilerargs.jaxws" value="-Djava.endorsed.dirs='${jaxws.endorsed.dir}'">
29.137 + <and>
29.138 + <isset property="jaxws.endorsed.dir"/>
29.139 + <available file="nbproject/jaxws-build.xml"/>
29.140 + </and>
29.141 + </condition>
29.142 + </target>
29.143 + <target name="-post-init">
29.144 + <!-- Empty placeholder for easier customization. -->
29.145 + <!-- You can override this target in the ../build.xml file. -->
29.146 + </target>
29.147 + <target depends="-pre-init,-init-private,-init-user,-init-project,-do-init" name="-init-check">
29.148 + <fail unless="src.dir">Must set src.dir</fail>
29.149 + <fail unless="build.dir">Must set build.dir</fail>
29.150 + <fail unless="dist.dir">Must set dist.dir</fail>
29.151 + <fail unless="build.classes.dir">Must set build.classes.dir</fail>
29.152 + <fail unless="dist.javadoc.dir">Must set dist.javadoc.dir</fail>
29.153 + <fail unless="build.test.classes.dir">Must set build.test.classes.dir</fail>
29.154 + <fail unless="build.test.results.dir">Must set build.test.results.dir</fail>
29.155 + <fail unless="build.classes.excludes">Must set build.classes.excludes</fail>
29.156 + <fail unless="dist.jar">Must set dist.jar</fail>
29.157 + </target>
29.158 + <target name="-init-macrodef-property">
29.159 + <macrodef name="property" uri="http://www.netbeans.org/ns/scala-project/1">
29.160 + <attribute name="name"/>
29.161 + <attribute name="value"/>
29.162 + <sequential>
29.163 + <property name="@{name}" value="${@{value}}"/>
29.164 + </sequential>
29.165 + </macrodef>
29.166 + </target>
29.167 + <target name="-init-macrodef-javac">
29.168 + <macrodef name="javac" uri="http://www.netbeans.org/ns/scala-project/1">
29.169 + <attribute default="${src.dir}" name="srcdir"/>
29.170 + <attribute default="${build.classes.dir}" name="destdir"/>
29.171 + <attribute default="${javac.classpath}" name="classpath"/>
29.172 + <attribute default="${includes}" name="includes"/>
29.173 + <attribute default="${excludes}" name="excludes"/>
29.174 + <attribute default="${javac.debug}" name="debug"/>
29.175 + <attribute default="" name="sourcepath"/>
29.176 + <element name="customize" optional="true"/>
29.177 + <sequential>
29.178 + <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}">
29.179 + <classpath>
29.180 + <path path="@{classpath}"/>
29.181 + <fileset dir="${scala.lib}">
29.182 + <include name="**/*.jar"/>
29.183 + </fileset>
29.184 + </classpath>
29.185 + <compilerarg line="${javac.compilerargs} ${javac.compilerargs.jaxws}"/>
29.186 + <customize/>
29.187 + </javac>
29.188 + </sequential>
29.189 + </macrodef>
29.190 + <macrodef name="depend" uri="http://www.netbeans.org/ns/scala-project/1">
29.191 + <attribute default="${src.dir}" name="srcdir"/>
29.192 + <attribute default="${build.classes.dir}" name="destdir"/>
29.193 + <attribute default="${javac.classpath}" name="classpath"/>
29.194 + <sequential>
29.195 + <depend cache="${build.dir}/depcache" destdir="@{destdir}" excludes="${excludes}" includes="${includes}" srcdir="@{srcdir}">
29.196 + <classpath>
29.197 + <path path="@{classpath}"/>
29.198 + </classpath>
29.199 + </depend>
29.200 + </sequential>
29.201 + </macrodef>
29.202 + <macrodef name="force-recompile" uri="http://www.netbeans.org/ns/scala-project/1">
29.203 + <attribute default="${build.classes.dir}" name="destdir"/>
29.204 + <sequential>
29.205 + <fail unless="javac.includes">Must set javac.includes</fail>
29.206 + <pathconvert pathsep="," property="javac.includes.binary">
29.207 + <path>
29.208 + <filelist dir="@{destdir}" files="${javac.includes}"/>
29.209 + </path>
29.210 + <globmapper from="*.java" to="*.class"/>
29.211 + </pathconvert>
29.212 + <delete>
29.213 + <files includes="${javac.includes.binary}"/>
29.214 + </delete>
29.215 + </sequential>
29.216 + </macrodef>
29.217 + </target>
29.218 + <target name="-init-macrodef-scalac">
29.219 + <macrodef name="scalac" uri="http://www.netbeans.org/ns/scala-project/1">
29.220 + <attribute default="${src.dir}" name="srcdir"/>
29.221 + <attribute default="${build.classes.dir}" name="destdir"/>
29.222 + <attribute default="${javac.classpath}" name="classpath"/>
29.223 + <attribute default="${includes}" name="includes"/>
29.224 + <attribute default="${excludes}" name="excludes"/>
29.225 + <attribute default="${javac.compilerargs}" name="addparams"/>
29.226 + <attribute default="" name="sourcepath"/>
29.227 + <element name="customize" optional="true"/>
29.228 + <sequential>
29.229 + <fsc addparams="@{addparams}" destdir="@{destdir}" encoding="${source.encoding}" excludes="@{excludes}" includes="@{includes}" sourcepath="@{sourcepath}" srcdir="@{srcdir}" target="jvm-${javac.target}">
29.230 + <classpath>
29.231 + <path path="@{classpath}"/>
29.232 + <fileset dir="${scala.lib}">
29.233 + <include name="**/*.jar"/>
29.234 + </fileset>
29.235 + </classpath>
29.236 + <customize/>
29.237 + </fsc>
29.238 + </sequential>
29.239 + </macrodef>
29.240 + <macrodef name="depend" uri="http://www.netbeans.org/ns/scala-project/1">
29.241 + <attribute default="${src.dir}" name="srcdir"/>
29.242 + <attribute default="${build.classes.dir}" name="destdir"/>
29.243 + <attribute default="${javac.classpath}" name="classpath"/>
29.244 + <sequential>
29.245 + <depend cache="${build.dir}/depcache" destdir="@{destdir}" excludes="${excludes}" includes="${includes}" srcdir="@{srcdir}">
29.246 + <classpath>
29.247 + <path path="@{classpath}"/>
29.248 + </classpath>
29.249 + </depend>
29.250 + </sequential>
29.251 + </macrodef>
29.252 + <macrodef name="force-recompile" uri="http://www.netbeans.org/ns/scala-project/1">
29.253 + <attribute default="${build.classes.dir}" name="destdir"/>
29.254 + <sequential>
29.255 + <fail unless="javac.includes">Must set javac.includes</fail>
29.256 + <pathconvert pathsep="," property="javac.includes.binary">
29.257 + <path>
29.258 + <filelist dir="@{destdir}" files="${javac.includes}"/>
29.259 + </path>
29.260 + <globmapper from="*.scala" to="*.class"/>
29.261 + </pathconvert>
29.262 + <delete>
29.263 + <files includes="${javac.includes.binary}"/>
29.264 + </delete>
29.265 + </sequential>
29.266 + </macrodef>
29.267 + </target>
29.268 + <target name="-init-macrodef-junit">
29.269 + <macrodef name="junit" uri="http://www.netbeans.org/ns/scala-project/1">
29.270 + <attribute default="${includes}" name="includes"/>
29.271 + <attribute default="${excludes}" name="excludes"/>
29.272 + <attribute default="**" name="testincludes"/>
29.273 + <sequential>
29.274 + <junit dir="${work.dir}" errorproperty="tests.failed" failureproperty="tests.failed" fork="true" showoutput="true">
29.275 + <batchtest todir="${build.test.results.dir}">
29.276 + <fileset dir="${build.test.classes.dir}" excludes="@{excludes},${excludes}" includes="@{includes}">
29.277 + <filename name="@{testincludes}"/>
29.278 + </fileset>
29.279 + </batchtest>
29.280 + <classpath>
29.281 + <path path="${run.test.classpath}"/>
29.282 + <fileset dir="${scala.lib}">
29.283 + <include name="**/*.jar"/>
29.284 + </fileset>
29.285 + </classpath>
29.286 + <syspropertyset>
29.287 + <propertyref prefix="test-sys-prop."/>
29.288 + <mapper from="test-sys-prop.*" to="*" type="glob"/>
29.289 + </syspropertyset>
29.290 + <formatter type="brief" usefile="false"/>
29.291 + <formatter type="xml"/>
29.292 + <jvmarg line="${run.jvmargs}"/>
29.293 + </junit>
29.294 + </sequential>
29.295 + </macrodef>
29.296 + </target>
29.297 + <target name="-init-macrodef-nbjpda">
29.298 + <macrodef name="nbjpdastart" uri="http://www.netbeans.org/ns/scala-project/1">
29.299 + <attribute default="${main.class}" name="name"/>
29.300 + <attribute default="${debug.classpath}" name="classpath"/>
29.301 + <attribute default="" name="stopclassname"/>
29.302 + <sequential>
29.303 + <nbjpdastart addressproperty="jpda.address" name="@{name}" stopclassname="@{stopclassname}" transport="dt_socket">
29.304 + <classpath>
29.305 + <path path="@{classpath}"/>
29.306 + </classpath>
29.307 + </nbjpdastart>
29.308 + </sequential>
29.309 + </macrodef>
29.310 + <macrodef name="nbjpdareload" uri="http://www.netbeans.org/ns/scala-project/1">
29.311 + <attribute default="${build.classes.dir}" name="dir"/>
29.312 + <sequential>
29.313 + <nbjpdareload>
29.314 + <fileset dir="@{dir}" includes="${fix.includes}*.class"/>
29.315 + </nbjpdareload>
29.316 + </sequential>
29.317 + </macrodef>
29.318 + </target>
29.319 + <target name="-init-debug-args">
29.320 + <property name="version-output" value="java version "${ant.java.version}"/>
29.321 + <condition property="have-jdk-older-than-1.4">
29.322 + <or>
29.323 + <contains string="${version-output}" substring="java version "1.0"/>
29.324 + <contains string="${version-output}" substring="java version "1.1"/>
29.325 + <contains string="${version-output}" substring="java version "1.2"/>
29.326 + <contains string="${version-output}" substring="java version "1.3"/>
29.327 + </or>
29.328 + </condition>
29.329 + <condition else="-Xdebug" property="debug-args-line" value="-Xdebug -Xnoagent -Djava.compiler=none">
29.330 + <istrue value="${have-jdk-older-than-1.4}"/>
29.331 + </condition>
29.332 + </target>
29.333 + <target depends="-init-debug-args" name="-init-macrodef-debug">
29.334 + <macrodef name="debug" uri="http://www.netbeans.org/ns/scala-project/1">
29.335 + <attribute default="${main.class}" name="classname"/>
29.336 + <attribute default="${debug.classpath}" name="classpath"/>
29.337 + <element name="customize" optional="true"/>
29.338 + <sequential>
29.339 + <java classname="@{classname}" dir="${work.dir}" fork="true">
29.340 + <jvmarg line="${debug-args-line}"/>
29.341 + <jvmarg value="-Xrunjdwp:transport=dt_socket,address=${jpda.address}"/>
29.342 + <jvmarg line="${run.jvmargs}"/>
29.343 + <classpath>
29.344 + <path path="@{classpath}"/>
29.345 + <fileset dir="${scala.lib}">
29.346 + <include name="**/*.jar"/>
29.347 + </fileset>
29.348 + </classpath>
29.349 + <syspropertyset>
29.350 + <propertyref prefix="run-sys-prop."/>
29.351 + <mapper from="run-sys-prop.*" to="*" type="glob"/>
29.352 + </syspropertyset>
29.353 + <customize/>
29.354 + </java>
29.355 + </sequential>
29.356 + </macrodef>
29.357 + </target>
29.358 + <target name="-init-macrodef-java">
29.359 + <macrodef name="java" uri="http://www.netbeans.org/ns/scala-project/1">
29.360 + <attribute default="${main.class}" name="classname"/>
29.361 + <element name="customize" optional="true"/>
29.362 + <sequential>
29.363 + <java classname="@{classname}" dir="${work.dir}" fork="true">
29.364 + <jvmarg line="${run.jvmargs}"/>
29.365 + <classpath>
29.366 + <path path="${run.classpath}"/>
29.367 + <fileset dir="${scala.lib}">
29.368 + <include name="**/*.jar"/>
29.369 + </fileset>
29.370 + </classpath>
29.371 + <syspropertyset>
29.372 + <propertyref prefix="run-sys-prop."/>
29.373 + <mapper from="run-sys-prop.*" to="*" type="glob"/>
29.374 + </syspropertyset>
29.375 + <customize/>
29.376 + </java>
29.377 + </sequential>
29.378 + </macrodef>
29.379 + </target>
29.380 + <target name="-init-presetdef-jar">
29.381 + <presetdef name="jar" uri="http://www.netbeans.org/ns/scala-project/1">
29.382 + <jar compress="${jar.compress}" jarfile="${dist.jar}">
29.383 + <scalaProject1:fileset dir="${build.classes.dir}"/>
29.384 + </jar>
29.385 + </presetdef>
29.386 + </target>
29.387 + <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"/>
29.388 + <!--
29.389 + ===================
29.390 + COMPILATION SECTION
29.391 + ===================
29.392 + -->
29.393 + <target depends="init" name="deps-jar" unless="no.deps">
29.394 + <ant antfile="${project.jEdit}/build-nb.xml" inheritall="false" target="build"/>
29.395 + </target>
29.396 + <target depends="init,deps-jar" name="-pre-pre-compile">
29.397 + <mkdir dir="${build.classes.dir}"/>
29.398 + </target>
29.399 + <target name="-pre-compile">
29.400 + <!-- Empty placeholder for easier customization. -->
29.401 + <!-- You can override this target in the ../build.xml file. -->
29.402 + </target>
29.403 + <target if="do.depend.true" name="-compile-depend">
29.404 + <scalaProject1:depend/>
29.405 + </target>
29.406 + <target depends="init,deps-jar,-pre-pre-compile,-pre-compile,-compile-depend" if="have.sources" name="-do-compile">
29.407 + <scalaProject1:scalac/>
29.408 + <scalaProject1:javac/>
29.409 + <copy todir="${build.classes.dir}">
29.410 + <fileset dir="${src.dir}" excludes="${build.classes.excludes},${excludes} " includes="${includes}"/>
29.411 + </copy>
29.412 + </target>
29.413 + <target name="-post-compile">
29.414 + <!-- Empty placeholder for easier customization. -->
29.415 + <!-- You can override this target in the ../build.xml file. -->
29.416 + </target>
29.417 + <target depends="init,deps-jar,-pre-pre-compile,-pre-compile,-do-compile,-post-compile" description="Compile project." name="compile"/>
29.418 + <target name="-pre-compile-single">
29.419 + <!-- Empty placeholder for easier customization. -->
29.420 + <!-- You can override this target in the ../build.xml file. -->
29.421 + </target>
29.422 + <target depends="init,deps-jar,-pre-pre-compile" name="-do-compile-single">
29.423 + <fail unless="javac.includes">Must select some files in the IDE or set javac.includes</fail>
29.424 + <scalaProject1:force-recompile/>
29.425 + <scalaProject1:scalac excludes="" includes="${javac.includes}" sourcepath="${src.dir}"/>
29.426 + </target>
29.427 + <target name="-post-compile-single">
29.428 + <!-- Empty placeholder for easier customization. -->
29.429 + <!-- You can override this target in the ../build.xml file. -->
29.430 + </target>
29.431 + <target depends="init,deps-jar,-pre-pre-compile,-pre-compile-single,-do-compile-single,-post-compile-single" name="compile-single"/>
29.432 + <!--
29.433 + ====================
29.434 + JAR BUILDING SECTION
29.435 + ====================
29.436 + -->
29.437 + <target depends="init" name="-pre-pre-jar">
29.438 + <dirname file="${dist.jar}" property="dist.jar.dir"/>
29.439 + <mkdir dir="${dist.jar.dir}"/>
29.440 + </target>
29.441 + <target name="-pre-jar">
29.442 + <!-- Empty placeholder for easier customization. -->
29.443 + <!-- You can override this target in the ../build.xml file. -->
29.444 + </target>
29.445 + <target depends="init,compile,-pre-pre-jar,-pre-jar" name="-do-jar-without-manifest" unless="manifest.available">
29.446 + <scalaProject1:jar/>
29.447 + </target>
29.448 + <target depends="init,compile,-pre-pre-jar,-pre-jar" if="manifest.available" name="-do-jar-with-manifest" unless="manifest.available+main.class">
29.449 + <scalaProject1:jar manifest="${manifest.file}"/>
29.450 + </target>
29.451 + <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">
29.452 + <scalaProject1:jar manifest="${manifest.file}">
29.453 + <scalaProject1:manifest>
29.454 + <scalaProject1:attribute name="Main-Class" value="${main.class}"/>
29.455 + </scalaProject1:manifest>
29.456 + </scalaProject1:jar>
29.457 + <echo>To run this application from the command line without Ant, try:</echo>
29.458 + <property location="${build.classes.dir}" name="build.classes.dir.resolved"/>
29.459 + <property location="${dist.jar}" name="dist.jar.resolved"/>
29.460 + <pathconvert property="run.classpath.with.dist.jar">
29.461 + <path path="${run.classpath}"/>
29.462 + <map from="${build.classes.dir.resolved}" to="${dist.jar.resolved}"/>
29.463 + </pathconvert>
29.464 + <echo>java -cp "${run.classpath.with.dist.jar}" ${main.class}
29.465 + </echo>
29.466 + </target>
29.467 + <target depends="init,compile,-pre-pre-jar,-pre-jar" if="manifest.available+main.class+mkdist.available" name="-do-jar-with-libraries">
29.468 + <property location="${build.classes.dir}" name="build.classes.dir.resolved"/>
29.469 + <pathconvert property="run.classpath.without.build.classes.dir">
29.470 + <path path="${run.classpath}"/>
29.471 + <map from="${build.classes.dir.resolved}" to=""/>
29.472 + </pathconvert>
29.473 + <pathconvert pathsep=" " property="jar.classpath">
29.474 + <path path="${run.classpath.without.build.classes.dir}"/>
29.475 + <chainedmapper>
29.476 + <flattenmapper/>
29.477 + <globmapper from="*" to="lib/*"/>
29.478 + </chainedmapper>
29.479 + </pathconvert>
29.480 + <taskdef classname="org.netbeans.modules.java.j2seproject.copylibstask.CopyLibs" classpath="${libs.CopyLibs.classpath}" name="copylibs"/>
29.481 + <copylibs compress="${jar.compress}" jarfile="${dist.jar}" manifest="${manifest.file}" runtimeclasspath="${run.classpath.without.build.classes.dir}">
29.482 + <fileset dir="${build.classes.dir}"/>
29.483 + <manifest>
29.484 + <attribute name="Main-Class" value="${main.class}"/>
29.485 + <attribute name="Class-Path" value="${jar.classpath}"/>
29.486 + </manifest>
29.487 + </copylibs>
29.488 + <echo>To run this application from the command line without Ant, try:</echo>
29.489 + <property location="${dist.jar}" name="dist.jar.resolved"/>
29.490 + <echo>java -jar "${dist.jar.resolved}"
29.491 + </echo>
29.492 + </target>
29.493 + <target name="-post-jar">
29.494 + <!-- Empty placeholder for easier customization. -->
29.495 + <!-- You can override this target in the ../build.xml file. -->
29.496 + </target>
29.497 + <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"/>
29.498 + <!--
29.499 + =================
29.500 + EXECUTION SECTION
29.501 + =================
29.502 + -->
29.503 + <target depends="init,compile" description="Run a main class." name="run">
29.504 + <scalaProject1:java>
29.505 + <customize>
29.506 + <arg line="${application.args}"/>
29.507 + </customize>
29.508 + </scalaProject1:java>
29.509 + </target>
29.510 + <target name="-do-not-recompile">
29.511 + <property name="javac.includes.binary" value=""/>
29.512 + </target>
29.513 + <target depends="init,-do-not-recompile,compile-single" name="run-single">
29.514 + <fail unless="run.class">Must select one file in the IDE or set run.class</fail>
29.515 + <scalaProject1:java classname="${run.class}"/>
29.516 + </target>
29.517 + <!--
29.518 + =================
29.519 + DEBUGGING SECTION
29.520 + =================
29.521 + -->
29.522 + <target depends="init" if="netbeans.home" name="-debug-start-debugger">
29.523 + <scalaProject1:nbjpdastart name="${debug.class}"/>
29.524 + </target>
29.525 + <target depends="init,compile" name="-debug-start-debuggee">
29.526 + <scalaProject1:debug>
29.527 + <customize>
29.528 + <arg line="${application.args}"/>
29.529 + </customize>
29.530 + </scalaProject1:debug>
29.531 + </target>
29.532 + <target depends="init,compile,-debug-start-debugger,-debug-start-debuggee" description="Debug project in IDE." if="netbeans.home" name="debug"/>
29.533 + <target depends="init" if="netbeans.home" name="-debug-start-debugger-stepinto">
29.534 + <scalaProject1:nbjpdastart stopclassname="${main.class}"/>
29.535 + </target>
29.536 + <target depends="init,compile,-debug-start-debugger-stepinto,-debug-start-debuggee" if="netbeans.home" name="debug-stepinto"/>
29.537 + <target depends="init,compile-single" if="netbeans.home" name="-debug-start-debuggee-single">
29.538 + <fail unless="debug.class">Must select one file in the IDE or set debug.class</fail>
29.539 + <scalaProject1:debug classname="${debug.class}"/>
29.540 + </target>
29.541 + <target depends="init,-do-not-recompile,compile-single,-debug-start-debugger,-debug-start-debuggee-single" if="netbeans.home" name="debug-single"/>
29.542 + <target depends="init" name="-pre-debug-fix">
29.543 + <fail unless="fix.includes">Must set fix.includes</fail>
29.544 + <property name="javac.includes" value="${fix.includes}.java"/>
29.545 + </target>
29.546 + <target depends="init,-pre-debug-fix,compile-single" if="netbeans.home" name="-do-debug-fix">
29.547 + <scalaProject1:nbjpdareload/>
29.548 + </target>
29.549 + <target depends="init,-pre-debug-fix,-do-debug-fix" if="netbeans.home" name="debug-fix"/>
29.550 + <!--
29.551 + ===============
29.552 + JAVADOC SECTION
29.553 + ===============
29.554 + -->
29.555 + <target depends="init" name="-javadoc-build">
29.556 + <mkdir dir="${dist.javadoc.dir}"/>
29.557 + <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}">
29.558 + <classpath>
29.559 + <path path="${javac.classpath}"/>
29.560 + </classpath>
29.561 + <fileset dir="${src.dir}" excludes="${excludes}" includes="${includes}">
29.562 + <filename name="**/*.java"/>
29.563 + </fileset>
29.564 + </javadoc>
29.565 + </target>
29.566 + <target depends="init,-javadoc-build" if="netbeans.home" name="-javadoc-browse" unless="no.javadoc.preview">
29.567 + <nbbrowse file="${dist.javadoc.dir}/index.html"/>
29.568 + </target>
29.569 + <target depends="init,-javadoc-build,-javadoc-browse" description="Build Javadoc." name="javadoc"/>
29.570 + <!--
29.571 + =========================
29.572 + JUNIT COMPILATION SECTION
29.573 + =========================
29.574 + -->
29.575 + <target depends="init,compile" if="have.tests" name="-pre-pre-compile-test">
29.576 + <mkdir dir="${build.test.classes.dir}"/>
29.577 + </target>
29.578 + <target name="-pre-compile-test">
29.579 + <!-- Empty placeholder for easier customization. -->
29.580 + <!-- You can override this target in the ../build.xml file. -->
29.581 + </target>
29.582 + <target if="do.depend.true" name="-compile-test-depend">
29.583 + <scalaProject1:depend classpath="${javac.test.classpath}" destdir="${build.test.classes.dir}" srcdir=""/>
29.584 + </target>
29.585 + <target depends="init,compile,-pre-pre-compile-test,-pre-compile-test,-compile-test-depend" if="have.tests" name="-do-compile-test">
29.586 + <scalaProject1:scalac classpath="${javac.test.classpath}" debug="true" destdir="${build.test.classes.dir}" srcdir=""/>
29.587 + <copy todir="${build.test.classes.dir}"/>
29.588 + </target>
29.589 + <target name="-post-compile-test">
29.590 + <!-- Empty placeholder for easier customization. -->
29.591 + <!-- You can override this target in the ../build.xml file. -->
29.592 + </target>
29.593 + <target depends="init,compile,-pre-pre-compile-test,-pre-compile-test,-do-compile-test,-post-compile-test" name="compile-test"/>
29.594 + <target name="-pre-compile-test-single">
29.595 + <!-- Empty placeholder for easier customization. -->
29.596 + <!-- You can override this target in the ../build.xml file. -->
29.597 + </target>
29.598 + <target depends="init,compile,-pre-pre-compile-test,-pre-compile-test-single" if="have.tests" name="-do-compile-test-single">
29.599 + <fail unless="javac.includes">Must select some files in the IDE or set javac.includes</fail>
29.600 + <scalaProject1:force-recompile destdir="${build.test.classes.dir}"/>
29.601 + <scalaProject1:scalac classpath="${javac.test.classpath}" debug="true" destdir="${build.test.classes.dir}" excludes="" includes="${javac.includes}" sourcepath="" srcdir=""/>
29.602 + <copy todir="${build.test.classes.dir}"/>
29.603 + </target>
29.604 + <target name="-post-compile-test-single">
29.605 + <!-- Empty placeholder for easier customization. -->
29.606 + <!-- You can override this target in the ../build.xml file. -->
29.607 + </target>
29.608 + <target depends="init,compile,-pre-pre-compile-test,-pre-compile-test-single,-do-compile-test-single,-post-compile-test-single" name="compile-test-single"/>
29.609 + <!--
29.610 + =======================
29.611 + JUNIT EXECUTION SECTION
29.612 + =======================
29.613 + -->
29.614 + <target depends="init" if="have.tests" name="-pre-test-run">
29.615 + <mkdir dir="${build.test.results.dir}"/>
29.616 + </target>
29.617 + <target depends="init,compile-test,-pre-test-run" if="have.tests" name="-do-test-run">
29.618 + <scalaProject1:junit testincludes="**/*Test.class"/>
29.619 + </target>
29.620 + <target depends="init,compile-test,-pre-test-run,-do-test-run" if="have.tests" name="-post-test-run">
29.621 + <fail if="tests.failed">Some tests failed; see details above.</fail>
29.622 + </target>
29.623 + <target depends="init" if="have.tests" name="test-report"/>
29.624 + <target depends="init" if="netbeans.home+have.tests" name="-test-browse"/>
29.625 + <target depends="init,compile-test,-pre-test-run,-do-test-run,test-report,-post-test-run,-test-browse" description="Run unit tests." name="test"/>
29.626 + <target depends="init" if="have.tests" name="-pre-test-run-single">
29.627 + <mkdir dir="${build.test.results.dir}"/>
29.628 + </target>
29.629 + <target depends="init,compile-test-single,-pre-test-run-single" if="have.tests" name="-do-test-run-single">
29.630 + <fail unless="test.includes">Must select some files in the IDE or set test.includes</fail>
29.631 + <scalaProject1:junit excludes="" includes="${test.includes}"/>
29.632 + </target>
29.633 + <target depends="init,compile-test-single,-pre-test-run-single,-do-test-run-single" if="have.tests" name="-post-test-run-single">
29.634 + <fail if="tests.failed">Some tests failed; see details above.</fail>
29.635 + </target>
29.636 + <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"/>
29.637 + <!--
29.638 + =======================
29.639 + JUNIT DEBUGGING SECTION
29.640 + =======================
29.641 + -->
29.642 + <target depends="init,compile-test" if="have.tests" name="-debug-start-debuggee-test">
29.643 + <fail unless="test.class">Must select one file in the IDE or set test.class</fail>
29.644 + <property location="${build.test.results.dir}/TEST-${test.class}.xml" name="test.report.file"/>
29.645 + <delete file="${test.report.file}"/>
29.646 + <mkdir dir="${build.test.results.dir}"/>
29.647 + <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}">
29.648 + <customize>
29.649 + <syspropertyset>
29.650 + <propertyref prefix="test-sys-prop."/>
29.651 + <mapper from="test-sys-prop.*" to="*" type="glob"/>
29.652 + </syspropertyset>
29.653 + <arg value="${test.class}"/>
29.654 + <arg value="showoutput=true"/>
29.655 + <arg value="formatter=org.apache.tools.ant.taskdefs.optional.junit.BriefJUnitResultFormatter"/>
29.656 + <arg value="formatter=org.apache.tools.ant.taskdefs.optional.junit.XMLJUnitResultFormatter,${test.report.file}"/>
29.657 + </customize>
29.658 + </scalaProject1:debug>
29.659 + </target>
29.660 + <target depends="init,compile-test" if="netbeans.home+have.tests" name="-debug-start-debugger-test">
29.661 + <scalaProject1:nbjpdastart classpath="${debug.test.classpath}" name="${test.class}"/>
29.662 + </target>
29.663 + <target depends="init,-do-not-recompile,compile-test-single,-debug-start-debugger-test,-debug-start-debuggee-test" name="debug-test"/>
29.664 + <target depends="init,-pre-debug-fix,compile-test-single" if="netbeans.home" name="-do-debug-fix-test">
29.665 + <scalaProject1:nbjpdareload dir="${build.test.classes.dir}"/>
29.666 + </target>
29.667 + <target depends="init,-pre-debug-fix,-do-debug-fix-test" if="netbeans.home" name="debug-fix-test"/>
29.668 + <!--
29.669 + =========================
29.670 + APPLET EXECUTION SECTION
29.671 + =========================
29.672 + -->
29.673 + <target depends="init,compile-single" name="run-applet">
29.674 + <fail unless="applet.url">Must select one file in the IDE or set applet.url</fail>
29.675 + <scalaProject1:java classname="sun.applet.AppletViewer">
29.676 + <customize>
29.677 + <arg value="${applet.url}"/>
29.678 + </customize>
29.679 + </scalaProject1:java>
29.680 + </target>
29.681 + <!--
29.682 + =========================
29.683 + APPLET DEBUGGING SECTION
29.684 + =========================
29.685 + -->
29.686 + <target depends="init,compile-single" if="netbeans.home" name="-debug-start-debuggee-applet">
29.687 + <fail unless="applet.url">Must select one file in the IDE or set applet.url</fail>
29.688 + <scalaProject1:debug classname="sun.applet.AppletViewer">
29.689 + <customize>
29.690 + <arg value="${applet.url}"/>
29.691 + </customize>
29.692 + </scalaProject1:debug>
29.693 + </target>
29.694 + <target depends="init,compile-single,-debug-start-debugger,-debug-start-debuggee-applet" if="netbeans.home" name="debug-applet"/>
29.695 + <!--
29.696 + ===============
29.697 + CLEANUP SECTION
29.698 + ===============
29.699 + -->
29.700 + <target depends="init" name="deps-clean" unless="no.deps">
29.701 + <ant antfile="${project.jEdit}/build-nb.xml" inheritall="false" target="clean"/>
29.702 + </target>
29.703 + <target depends="init" name="-do-clean">
29.704 + <delete dir="${build.dir}"/>
29.705 + <delete dir="${dist.dir}"/>
29.706 + </target>
29.707 + <target name="-post-clean">
29.708 + <!-- Empty placeholder for easier customization. -->
29.709 + <!-- You can override this target in the ../build.xml file. -->
29.710 + </target>
29.711 + <target depends="init,deps-clean,-do-clean,-post-clean" description="Clean build products." name="clean"/>
29.712 +</project>
30.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
30.2 +++ b/src/Tools/jEdit/nbproject/genfiles.properties Mon Jan 11 23:11:31 2010 +0100
30.3 @@ -0,0 +1,8 @@
30.4 +build.xml.data.CRC32=d2379ac2
30.5 +build.xml.script.CRC32=2db9d955
30.6 +build.xml.stylesheet.CRC32=ca9d572e
30.7 +# This file is used by a NetBeans-based IDE to track changes in generated files such as build-impl.xml.
30.8 +# Do not edit this file. You may delete it but then the IDE will never regenerate such files for you.
30.9 +nbproject/build-impl.xml.data.CRC32=8f41dcce
30.10 +nbproject/build-impl.xml.script.CRC32=69f2059c
30.11 +nbproject/build-impl.xml.stylesheet.CRC32=bc42a706@1.3.0
31.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
31.2 +++ b/src/Tools/jEdit/nbproject/project.properties Mon Jan 11 23:11:31 2010 +0100
31.3 @@ -0,0 +1,77 @@
31.4 +application.title=Isabelle-jEdit
31.5 +application.vendor=makarius
31.6 +application.args=-noserver -nobackground
31.7 +build.classes.dir=${build.dir}/classes
31.8 +build.classes.excludes=**/*.java,**/*.form,**/*.scala
31.9 +# This directory is removed when the project is cleaned:
31.10 +build.dir=build
31.11 +build.generated.dir=${build.dir}/generated
31.12 +# Only compile against the classpath explicitly listed here:
31.13 +build.sysclasspath=ignore
31.14 +build.test.classes.dir=${build.dir}/test/classes
31.15 +build.test.results.dir=${build.dir}/test/results
31.16 +debug.classpath=\
31.17 + ${run.classpath}
31.18 +debug.test.classpath=\
31.19 + ${run.test.classpath}
31.20 +# This directory is removed when the project is cleaned:
31.21 +dist.dir=dist
31.22 +# dist can be used as jEdits settings-directory;
31.23 +# jEdit searches for plugins in the 'jars' subdirectory
31.24 +# must include something like this to private.properties:
31.25 +# application.args=-noserver -nobackground -settings=/absolute/path/to/project/dist
31.26 +#
31.27 +dist.jar=${dist.dir}/jars/Isabelle-jEdit.jar
31.28 +dist.javadoc.dir=${dist.dir}/javadoc
31.29 +excludes=
31.30 +file.reference.isabelle-jedit-src=src
31.31 +file.reference.jedit.jar=/home/makarius/lib/jedit/current/jedit.jar
31.32 +includes=**
31.33 +jar.compress=false
31.34 +java.platform.active=java_default_platform
31.35 +javac.classpath=\
31.36 + ${reference.jEdit.build}:\
31.37 + ${libs.Isabelle-Pure.classpath}:\
31.38 + ${libs.Cobra-Renderer.classpath}:\
31.39 + ${libs.Rhino-JavaScript.classpath}:\
31.40 + ${libs.ErrorList.classpath}:\
31.41 + ${libs.Hyperlinks.classpath}:\
31.42 + ${libs.SideKick.classpath}:\
31.43 + ${libs.Console.classpath}:\
31.44 + ${libs.Scala-compiler.classpath}
31.45 +# Space-separated list of extra javac options
31.46 +javac.compilerargs=
31.47 +javac.deprecation=false
31.48 +javac.source=1.5
31.49 +javac.target=1.5
31.50 +javac.test.classpath=\
31.51 + ${javac.classpath}:\
31.52 + ${build.classes.dir}:\
31.53 + ${libs.junit.classpath}:\
31.54 + ${libs.junit_4.classpath}
31.55 +javadoc.additionalparam=
31.56 +javadoc.author=false
31.57 +javadoc.encoding=${source.encoding}
31.58 +javadoc.noindex=false
31.59 +javadoc.nonavbar=false
31.60 +javadoc.notree=false
31.61 +javadoc.private=false
31.62 +javadoc.splitindex=true
31.63 +javadoc.use=true
31.64 +javadoc.version=false
31.65 +javadoc.windowtitle=
31.66 +main.class=org.gjt.sp.jedit.jEdit
31.67 +manifest.file=manifest.mf
31.68 +meta.inf.dir=${src.dir}/META-INF
31.69 +platform.active=default_platform
31.70 +project.jEdit=contrib/jEdit
31.71 +reference.jEdit.build=${project.jEdit}/build/jEdit.jar
31.72 +run.classpath=\
31.73 + ${javac.classpath}:\
31.74 + ${build.classes.dir}
31.75 +run.jvmargs=-Xms128m -Xmx512m
31.76 +run.test.classpath=\
31.77 + ${javac.test.classpath}:\
31.78 + ${build.test.classes.dir}
31.79 +source.encoding=UTF-8
31.80 +src.dir=${file.reference.isabelle-jedit-src}
32.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
32.2 +++ b/src/Tools/jEdit/nbproject/project.xml Mon Jan 11 23:11:31 2010 +0100
32.3 @@ -0,0 +1,24 @@
32.4 +<?xml version="1.0" encoding="UTF-8"?>
32.5 +<project xmlns="http://www.netbeans.org/ns/project/1">
32.6 + <type>org.netbeans.modules.scala.project</type>
32.7 + <configuration>
32.8 + <data xmlns="http://www.netbeans.org/ns/scala-project/1">
32.9 + <name>Isabelle-jEdit</name>
32.10 + <minimum-ant-version>1.6.5</minimum-ant-version>
32.11 + <source-roots>
32.12 + <root id="src.dir"/>
32.13 + </source-roots>
32.14 + <test-roots/>
32.15 + </data>
32.16 + <references xmlns="http://www.netbeans.org/ns/ant-project-references/1">
32.17 + <reference>
32.18 + <foreign-project>jEdit</foreign-project>
32.19 + <artifact-type>jar</artifact-type>
32.20 + <script>build-nb.xml</script>
32.21 + <target>build</target>
32.22 + <clean-target>clean</clean-target>
32.23 + <id>build</id>
32.24 + </reference>
32.25 + </references>
32.26 + </configuration>
32.27 +</project>
33.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
33.2 +++ b/src/Tools/jEdit/plugin/Isabelle.props Mon Jan 11 23:11:31 2010 +0100
33.3 @@ -0,0 +1,48 @@
33.4 +## Isabelle plugin properties
33.5 +##
33.6 +##:encoding=ISO-8859-1:
33.7 +
33.8 +#identification
33.9 +plugin.isabelle.jedit.Plugin.name=Isabelle
33.10 +plugin.isabelle.jedit.Plugin.author=Johannes Hölzl, Fabian Immler, Makarius Wenzel
33.11 +plugin.isabelle.jedit.Plugin.version=0.0.1
33.12 +plugin.isabelle.jedit.Plugin.description=Isabelle/Isar asynchronous proof processing
33.13 +
33.14 +#system parameters
33.15 +plugin.isabelle.jedit.Plugin.activate=startup
33.16 +plugin.isabelle.jedit.Plugin.usePluginHome=false
33.17 +
33.18 +#dependencies
33.19 +plugin.isabelle.jedit.Plugin.depend.0=jdk 1.6
33.20 +plugin.isabelle.jedit.Plugin.depend.1=jedit 04.03.17.00
33.21 +plugin.isabelle.jedit.Plugin.depend.2=plugin errorlist.ErrorListPlugin 1.7
33.22 +plugin.isabelle.jedit.Plugin.depend.3=plugin sidekick.SideKickPlugin 0.7.6
33.23 +plugin.isabelle.jedit.Plugin.depend.4=plugin gatchan.jedit.hyperlinks.HyperlinksPlugin 1.0.1
33.24 +
33.25 +#options
33.26 +plugin.isabelle.jedit.Plugin.option-pane=isabelle
33.27 +options.isabelle.label=Isabelle
33.28 +options.isabelle.code=new isabelle.jedit.Isabelle_Options();
33.29 +options.isabelle.logic.title=Logic
33.30 +options.isabelle.font-size.title=Font Size
33.31 +options.isabelle.font-size=14
33.32 +options.isabelle.startup-timeout=10000
33.33 +
33.34 +#menu actions
33.35 +plugin.isabelle.jedit.Plugin.menu.label=Isabelle
33.36 +plugin.isabelle.jedit.Plugin.menu=isabelle.activate isabelle.show-output isabelle.show-protocol
33.37 +isabelle.activate.label=Activate current buffer
33.38 +isabelle.show-output.label=Show Output
33.39 +isabelle.show-protocol.label=Show Protocol
33.40 +
33.41 +#dockables
33.42 +isabelle-output.title=Output
33.43 +isabelle-protocol.title=Protocol
33.44 +
33.45 +#SideKick
33.46 +sidekick.parser.isabelle.label=Isabelle
33.47 +mode.isabelle.sidekick.parser=isabelle
33.48 +mode.ml.sidekick.parser=isabelle
33.49 +
33.50 +#Hyperlinks
33.51 +mode.isabelle.hyperlink.source=isabelle
34.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
34.2 +++ b/src/Tools/jEdit/plugin/actions.xml Mon Jan 11 23:11:31 2010 +0100
34.3 @@ -0,0 +1,23 @@
34.4 +<?xml version="1.0"?>
34.5 +<!DOCTYPE ACTIONS SYSTEM "actions.dtd">
34.6 +
34.7 +<ACTIONS>
34.8 + <ACTION NAME="isabelle.activate">
34.9 + <CODE>
34.10 + isabelle.jedit.Isabelle.switch_active(view);
34.11 + </CODE>
34.12 + <IS_SELECTED>
34.13 + return isabelle.jedit.Isabelle.is_active(view);
34.14 + </IS_SELECTED>
34.15 + </ACTION>
34.16 + <ACTION NAME="isabelle.show-output">
34.17 + <CODE>
34.18 + wm.addDockableWindow("isabelle-output");
34.19 + </CODE>
34.20 + </ACTION>
34.21 + <ACTION NAME="isabelle.show-protocol">
34.22 + <CODE>
34.23 + wm.addDockableWindow("isabelle-protocol");
34.24 + </CODE>
34.25 + </ACTION>
34.26 +</ACTIONS>
34.27 \ No newline at end of file
35.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
35.2 +++ b/src/Tools/jEdit/plugin/dockables.xml Mon Jan 11 23:11:31 2010 +0100
35.3 @@ -0,0 +1,11 @@
35.4 +<?xml version="1.0"?>
35.5 +<!DOCTYPE DOCKABLES SYSTEM "dockables.dtd">
35.6 +
35.7 +<DOCKABLES>
35.8 + <DOCKABLE NAME="isabelle-output" MOVABLE="TRUE">
35.9 + new isabelle.jedit.Output_Dockable(view, position);
35.10 + </DOCKABLE>
35.11 + <DOCKABLE NAME="isabelle-protocol" MOVABLE="TRUE">
35.12 + new isabelle.jedit.Protocol_Dockable(view, position);
35.13 + </DOCKABLE>
35.14 +</DOCKABLES>
35.15 \ No newline at end of file
36.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
36.2 +++ b/src/Tools/jEdit/plugin/services.xml Mon Jan 11 23:11:31 2010 +0100
36.3 @@ -0,0 +1,17 @@
36.4 +<?xml version="1.0"?>
36.5 +<!DOCTYPE SERVICES SYSTEM "services.dtd">
36.6 +
36.7 +<SERVICES>
36.8 + <SERVICE NAME="UTF-8-Isabelle" CLASS="org.gjt.sp.jedit.io.Encoding">
36.9 + new isabelle.jedit.Isabelle_Encoding();
36.10 + </SERVICE>
36.11 + <SERVICE NAME="isabelle" CLASS="sidekick.SideKickParser">
36.12 + new isabelle.jedit.Isabelle_Sidekick();
36.13 + </SERVICE>
36.14 + <SERVICE NAME="isabelle" CLASS="gatchan.jedit.hyperlinks.HyperlinkSource">
36.15 + new isabelle.jedit.Isabelle_Hyperlinks();
36.16 + </SERVICE>
36.17 + <SERVICE CLASS="console.Shell" NAME="Scala">
36.18 + new isabelle.jedit.Scala_Console();
36.19 + </SERVICE>
36.20 +</SERVICES>
37.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
37.2 +++ b/src/Tools/jEdit/src/Dummy.java Mon Jan 11 23:11:31 2010 +0100
37.3 @@ -0,0 +1,3 @@
37.4 +/* dummy class to make ant javadoc work */
37.5 +package isabelle;
37.6 +public class Dummy { }
38.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
38.2 +++ b/src/Tools/jEdit/src/jedit/document_model.scala Mon Jan 11 23:11:31 2010 +0100
38.3 @@ -0,0 +1,143 @@
38.4 +/*
38.5 + * Document model connected to jEdit buffer
38.6 + *
38.7 + * @author Fabian Immler, TU Munich
38.8 + * @author Makarius
38.9 + */
38.10 +
38.11 +package isabelle.jedit
38.12 +
38.13 +
38.14 +import scala.actors.Actor, Actor._
38.15 +import scala.collection.mutable
38.16 +
38.17 +import org.gjt.sp.jedit.Buffer
38.18 +import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer}
38.19 +import org.gjt.sp.jedit.syntax.{ModeProvider, SyntaxStyle}
38.20 +
38.21 +
38.22 +object Document_Model
38.23 +{
38.24 + /* document model of buffer */
38.25 +
38.26 + private val key = "isabelle.document_model"
38.27 +
38.28 + def init(session: Session, buffer: Buffer): Document_Model =
38.29 + {
38.30 + Swing_Thread.assert()
38.31 + val model = new Document_Model(session, buffer)
38.32 + buffer.setProperty(key, model)
38.33 + model.activate()
38.34 + model
38.35 + }
38.36 +
38.37 + def apply(buffer: Buffer): Option[Document_Model] =
38.38 + {
38.39 + Swing_Thread.assert()
38.40 + buffer.getProperty(key) match {
38.41 + case model: Document_Model => Some(model)
38.42 + case _ => None
38.43 + }
38.44 + }
38.45 +
38.46 + def exit(buffer: Buffer)
38.47 + {
38.48 + Swing_Thread.assert()
38.49 + apply(buffer) match {
38.50 + case None => error("No document model for buffer: " + buffer)
38.51 + case Some(model) =>
38.52 + model.deactivate()
38.53 + buffer.unsetProperty(key)
38.54 + }
38.55 + }
38.56 +}
38.57 +
38.58 +class Document_Model(val session: Session, val buffer: Buffer)
38.59 +{
38.60 + /* history */
38.61 +
38.62 + private val document_0 = session.begin_document(buffer.getName)
38.63 +
38.64 + @volatile private var history = // owned by Swing thread
38.65 + new Change(document_0.id, None, Nil, Future.value(Nil, document_0))
38.66 +
38.67 + def current_change(): Change = history
38.68 + def recent_document(): Document = current_change().ancestors.find(_.is_assigned).get.join_document
38.69 +
38.70 +
38.71 + /* transforming offsets */
38.72 +
38.73 + private def changes_from(doc: Document): List[Text_Edit] =
38.74 + {
38.75 + Swing_Thread.assert()
38.76 + (edits_buffer.toList /:
38.77 + current_change.ancestors.takeWhile(_.id != doc.id))((edits, change) => change.edits ::: edits)
38.78 + }
38.79 +
38.80 + def from_current(doc: Document, offset: Int): Int =
38.81 + (offset /: changes_from(doc).reverse) ((i, change) => change before i)
38.82 +
38.83 + def to_current(doc: Document, offset: Int): Int =
38.84 + (offset /: changes_from(doc)) ((i, change) => change after i)
38.85 +
38.86 + def lines_of_command(doc: Document, cmd: Command): (Int, Int) =
38.87 + {
38.88 + val start = doc.command_start(cmd).get // FIXME total?
38.89 + val stop = start + cmd.length
38.90 + (buffer.getLineOfOffset(to_current(doc, start)),
38.91 + buffer.getLineOfOffset(to_current(doc, stop)))
38.92 + }
38.93 +
38.94 +
38.95 + /* text edits */
38.96 +
38.97 + private val edits_buffer = new mutable.ListBuffer[Text_Edit] // owned by Swing thread
38.98 +
38.99 + private val edits_delay = Swing_Thread.delay_last(300) {
38.100 + if (!edits_buffer.isEmpty) {
38.101 + val new_change = current_change().edit(session, edits_buffer.toList)
38.102 + edits_buffer.clear
38.103 + history = new_change
38.104 + new_change.result.map(_ => session.input(new_change))
38.105 + }
38.106 + }
38.107 +
38.108 +
38.109 + /* buffer listener */
38.110 +
38.111 + private val buffer_listener: BufferListener = new BufferAdapter
38.112 + {
38.113 + override def contentInserted(buffer: JEditBuffer,
38.114 + start_line: Int, offset: Int, num_lines: Int, length: Int)
38.115 + {
38.116 + edits_buffer += new Text_Edit(true, offset, buffer.getText(offset, length))
38.117 + edits_delay()
38.118 + }
38.119 +
38.120 + override def preContentRemoved(buffer: JEditBuffer,
38.121 + start_line: Int, start: Int, num_lines: Int, removed_length: Int)
38.122 + {
38.123 + edits_buffer += new Text_Edit(false, start, buffer.getText(start, removed_length))
38.124 + edits_delay()
38.125 + }
38.126 + }
38.127 +
38.128 +
38.129 + /* activation */
38.130 +
38.131 + def activate()
38.132 + {
38.133 + buffer.setTokenMarker(new Isabelle_Token_Marker(this))
38.134 + buffer.addBufferListener(buffer_listener)
38.135 + buffer.propertiesChanged()
38.136 +
38.137 + edits_buffer += new Text_Edit(true, 0, buffer.getText(0, buffer.getLength))
38.138 + edits_delay()
38.139 + }
38.140 +
38.141 + def deactivate()
38.142 + {
38.143 + buffer.setTokenMarker(buffer.getMode.getTokenMarker)
38.144 + buffer.removeBufferListener(buffer_listener)
38.145 + }
38.146 +}
39.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
39.2 +++ b/src/Tools/jEdit/src/jedit/document_view.scala Mon Jan 11 23:11:31 2010 +0100
39.3 @@ -0,0 +1,301 @@
39.4 +/*
39.5 + * Document view connected to jEdit text area
39.6 + *
39.7 + * @author Fabian Immler, TU Munich
39.8 + * @author Makarius
39.9 + */
39.10 +
39.11 +package isabelle.jedit
39.12 +
39.13 +
39.14 +import scala.actors.Actor._
39.15 +
39.16 +import java.awt.event.{MouseAdapter, MouseEvent}
39.17 +import java.awt.{BorderLayout, Graphics, Dimension, Color, Graphics2D}
39.18 +import javax.swing.{JPanel, ToolTipManager}
39.19 +import javax.swing.event.{CaretListener, CaretEvent}
39.20 +
39.21 +import org.gjt.sp.jedit.gui.RolloverButton
39.22 +import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
39.23 +
39.24 +
39.25 +object Document_View
39.26 +{
39.27 + def choose_color(command: Command, doc: Document): Color =
39.28 + {
39.29 + doc.current_state(command).map(_.status) match {
39.30 + case Some(Command.Status.UNPROCESSED) => new Color(255, 228, 225)
39.31 + case Some(Command.Status.FINISHED) => new Color(234, 248, 255)
39.32 + case Some(Command.Status.FAILED) => new Color(255, 193, 193)
39.33 + case _ => Color.red
39.34 + }
39.35 + }
39.36 +
39.37 +
39.38 + /* document view of text area */
39.39 +
39.40 + private val key = new Object
39.41 +
39.42 + def init(model: Document_Model, text_area: TextArea): Document_View =
39.43 + {
39.44 + Swing_Thread.assert()
39.45 + val doc_view = new Document_View(model, text_area)
39.46 + text_area.putClientProperty(key, doc_view)
39.47 + doc_view.activate()
39.48 + doc_view
39.49 + }
39.50 +
39.51 + def apply(text_area: TextArea): Option[Document_View] =
39.52 + {
39.53 + Swing_Thread.assert()
39.54 + text_area.getClientProperty(key) match {
39.55 + case doc_view: Document_View => Some(doc_view)
39.56 + case _ => None
39.57 + }
39.58 + }
39.59 +
39.60 + def exit(text_area: TextArea)
39.61 + {
39.62 + Swing_Thread.assert()
39.63 + apply(text_area) match {
39.64 + case None => error("No document view for text area: " + text_area)
39.65 + case Some(doc_view) =>
39.66 + doc_view.deactivate()
39.67 + text_area.putClientProperty(key, null)
39.68 + }
39.69 + }
39.70 +}
39.71 +
39.72 +
39.73 +class Document_View(model: Document_Model, text_area: TextArea)
39.74 +{
39.75 + private val session = model.session
39.76 +
39.77 +
39.78 + /* visible document -- owned by Swing thread */
39.79 +
39.80 + @volatile private var document = model.recent_document()
39.81 +
39.82 +
39.83 + /* buffer of changed commands -- owned by Swing thread */
39.84 +
39.85 + @volatile private var changed_commands: Set[Command] = Set()
39.86 +
39.87 + private val changed_delay = Swing_Thread.delay_first(100) {
39.88 + if (!changed_commands.isEmpty) {
39.89 + document = model.recent_document()
39.90 + for (cmd <- changed_commands if document.commands.contains(cmd)) { // FIXME cover doc states as well!!?
39.91 + update_syntax(cmd)
39.92 + invalidate_line(cmd)
39.93 + overview.repaint()
39.94 + }
39.95 + changed_commands = Set()
39.96 + }
39.97 + }
39.98 +
39.99 +
39.100 + /* command change actor */
39.101 +
39.102 + private case object Exit
39.103 +
39.104 + private val command_change_actor = actor {
39.105 + loop {
39.106 + react {
39.107 + case command: Command => // FIXME rough filtering according to document family!?
39.108 + Swing_Thread.now {
39.109 + changed_commands += command
39.110 + changed_delay()
39.111 + }
39.112 +
39.113 + case Exit => reply(()); exit()
39.114 +
39.115 + case bad => System.err.println("command_change_actor: ignoring bad message " + bad)
39.116 + }
39.117 + }
39.118 + }
39.119 +
39.120 +
39.121 + /* text_area_extension */
39.122 +
39.123 + private val text_area_extension = new TextAreaExtension
39.124 + {
39.125 + override def paintValidLine(gfx: Graphics2D,
39.126 + screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
39.127 + {
39.128 + def from_current(pos: Int) = model.from_current(document, pos)
39.129 + def to_current(pos: Int) = model.to_current(document, pos)
39.130 + val metrics = text_area.getPainter.getFontMetrics
39.131 + val saved_color = gfx.getColor
39.132 + try {
39.133 + for ((command, command_start) <-
39.134 + document.command_range(from_current(start), from_current(end)))
39.135 + {
39.136 + val begin = start max to_current(command_start)
39.137 + val finish = (end - 1) min to_current(command_start + command.length)
39.138 + encolor(gfx, y, metrics.getHeight, begin, finish,
39.139 + Document_View.choose_color(command, document), true)
39.140 + }
39.141 + }
39.142 + finally { gfx.setColor(saved_color) }
39.143 + }
39.144 +
39.145 + override def getToolTipText(x: Int, y: Int): String =
39.146 + {
39.147 + val offset = model.from_current(document, text_area.xyToOffset(x, y))
39.148 + document.command_at(offset) match {
39.149 + case Some((command, command_start)) =>
39.150 + document.current_state(command).get.type_at(offset - command_start).getOrElse(null)
39.151 + case None => null
39.152 + }
39.153 + }
39.154 + }
39.155 +
39.156 +
39.157 + /* caret_listener */
39.158 +
39.159 + private var _selected_command: Command = null
39.160 + private def selected_command = _selected_command
39.161 + private def selected_command_=(cmd: Command)
39.162 + {
39.163 + _selected_command = cmd
39.164 + session.results.event(cmd)
39.165 + }
39.166 +
39.167 + private val caret_listener = new CaretListener
39.168 + {
39.169 + override def caretUpdate(e: CaretEvent)
39.170 + {
39.171 + document.command_at(e.getDot) match {
39.172 + case Some((command, command_start)) if (selected_command != command) =>
39.173 + selected_command = command
39.174 + case _ =>
39.175 + }
39.176 + }
39.177 + }
39.178 +
39.179 +
39.180 + /* (re)painting */
39.181 +
39.182 + private val update_delay = Swing_Thread.delay_first(500) { model.buffer.propertiesChanged() }
39.183 +
39.184 + private def update_syntax(cmd: Command)
39.185 + {
39.186 + val (line1, line2) = model.lines_of_command(document, cmd)
39.187 + if (line2 >= text_area.getFirstLine &&
39.188 + line1 <= text_area.getFirstLine + text_area.getVisibleLines)
39.189 + update_delay()
39.190 + }
39.191 +
39.192 + private def invalidate_line(cmd: Command) =
39.193 + {
39.194 + val (start, stop) = model.lines_of_command(document, cmd)
39.195 + text_area.invalidateLineRange(start, stop)
39.196 +
39.197 + if (selected_command == cmd)
39.198 + session.results.event(cmd)
39.199 + }
39.200 +
39.201 + private def invalidate_all() =
39.202 + text_area.invalidateLineRange(text_area.getFirstPhysicalLine,
39.203 + text_area.getLastPhysicalLine)
39.204 +
39.205 + private def encolor(gfx: Graphics2D,
39.206 + y: Int, height: Int, begin: Int, finish: Int, color: Color, fill: Boolean)
39.207 + {
39.208 + val start = text_area.offsetToXY(begin)
39.209 + val stop =
39.210 + if (finish < model.buffer.getLength) text_area.offsetToXY(finish)
39.211 + else {
39.212 + val p = text_area.offsetToXY(finish - 1)
39.213 + val metrics = text_area.getPainter.getFontMetrics
39.214 + p.x = p.x + (metrics.charWidth(' ') max metrics.getMaxAdvance)
39.215 + p
39.216 + }
39.217 +
39.218 + if (start != null && stop != null) {
39.219 + gfx.setColor(color)
39.220 + if (fill) gfx.fillRect(start.x, y, stop.x - start.x, height)
39.221 + else gfx.drawRect(start.x, y, stop.x - start.x, height)
39.222 + }
39.223 + }
39.224 +
39.225 +
39.226 + /* overview of command status left of scrollbar */
39.227 +
39.228 + private val overview = new JPanel(new BorderLayout)
39.229 + {
39.230 + private val WIDTH = 10
39.231 + private val HEIGHT = 2
39.232 +
39.233 + setPreferredSize(new Dimension(WIDTH, 0))
39.234 +
39.235 + setRequestFocusEnabled(false)
39.236 +
39.237 + addMouseListener(new MouseAdapter {
39.238 + override def mousePressed(event: MouseEvent) {
39.239 + val line = y_to_line(event.getY)
39.240 + if (line >= 0 && line < text_area.getLineCount)
39.241 + text_area.setCaretPosition(text_area.getLineStartOffset(line))
39.242 + }
39.243 + })
39.244 +
39.245 + override def addNotify() {
39.246 + super.addNotify()
39.247 + ToolTipManager.sharedInstance.registerComponent(this)
39.248 + }
39.249 +
39.250 + override def removeNotify() {
39.251 + ToolTipManager.sharedInstance.unregisterComponent(this)
39.252 + super.removeNotify
39.253 + }
39.254 +
39.255 + override def getToolTipText(event: MouseEvent): String =
39.256 + {
39.257 + val line = y_to_line(event.getY())
39.258 + if (line >= 0 && line < text_area.getLineCount) "<html><b>TODO:</b><br>Tooltip</html>"
39.259 + else ""
39.260 + }
39.261 +
39.262 + override def paintComponent(gfx: Graphics)
39.263 + {
39.264 + super.paintComponent(gfx)
39.265 + val buffer = model.buffer
39.266 +
39.267 + for ((command, start) <- document.command_range(0)) {
39.268 + val line1 = buffer.getLineOfOffset(model.to_current(document, start))
39.269 + val line2 = buffer.getLineOfOffset(model.to_current(document, start + command.length)) + 1
39.270 + val y = line_to_y(line1)
39.271 + val height = HEIGHT * (line2 - line1)
39.272 + gfx.setColor(Document_View.choose_color(command, document))
39.273 + gfx.fillRect(0, y, getWidth - 1, height)
39.274 + }
39.275 + }
39.276 +
39.277 + private def line_to_y(line: Int): Int =
39.278 + (line * getHeight) / (text_area.getBuffer.getLineCount max text_area.getVisibleLines)
39.279 +
39.280 + private def y_to_line(y: Int): Int =
39.281 + (y * (text_area.getBuffer.getLineCount max text_area.getVisibleLines)) / getHeight
39.282 + }
39.283 +
39.284 +
39.285 + /* activation */
39.286 +
39.287 + private def activate()
39.288 + {
39.289 + text_area.getPainter.
39.290 + addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension)
39.291 + text_area.addCaretListener(caret_listener)
39.292 + text_area.addLeftOfScrollBar(overview)
39.293 + session.command_change += command_change_actor
39.294 + }
39.295 +
39.296 + private def deactivate()
39.297 + {
39.298 + session.command_change -= command_change_actor
39.299 + command_change_actor !? Exit
39.300 + text_area.removeLeftOfScrollBar(overview)
39.301 + text_area.removeCaretListener(caret_listener)
39.302 + text_area.getPainter.removeExtension(text_area_extension)
39.303 + }
39.304 +}
39.305 \ No newline at end of file
40.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
40.2 +++ b/src/Tools/jEdit/src/jedit/html_panel.scala Mon Jan 11 23:11:31 2010 +0100
40.3 @@ -0,0 +1,140 @@
40.4 +/*
40.5 + * HTML panel based on Lobo/Cobra
40.6 + *
40.7 + * @author Makarius
40.8 + */
40.9 +
40.10 +package isabelle.jedit
40.11 +
40.12 +
40.13 +import java.io.StringReader
40.14 +import java.awt.{BorderLayout, Dimension}
40.15 +import java.awt.event.MouseEvent
40.16 +
40.17 +import javax.swing.{JButton, JPanel, JScrollPane}
40.18 +import java.util.logging.{Logger, Level}
40.19 +
40.20 +import org.w3c.dom.html2.HTMLElement
40.21 +
40.22 +import org.lobobrowser.html.parser.{DocumentBuilderImpl, InputSourceImpl}
40.23 +import org.lobobrowser.html.gui.HtmlPanel
40.24 +import org.lobobrowser.html.domimpl.{HTMLDocumentImpl, HTMLStyleElementImpl, NodeImpl}
40.25 +import org.lobobrowser.html.test.{SimpleHtmlRendererContext, SimpleUserAgentContext}
40.26 +
40.27 +import scala.io.Source
40.28 +import scala.actors.Actor._
40.29 +
40.30 +
40.31 +object HTML_Panel
40.32 +{
40.33 + sealed abstract class Event { val element: HTMLElement; val mouse: MouseEvent }
40.34 + case class Context_Menu(val element: HTMLElement, mouse: MouseEvent) extends Event
40.35 + case class Mouse_Click(val element: HTMLElement, mouse: MouseEvent) extends Event
40.36 + case class Double_Click(val element: HTMLElement, mouse: MouseEvent) extends Event
40.37 + case class Mouse_Over(val element: HTMLElement, mouse: MouseEvent) extends Event
40.38 + case class Mouse_Out(val element: HTMLElement, mouse: MouseEvent) extends Event
40.39 +}
40.40 +
40.41 +
40.42 +class HTML_Panel(
40.43 + sys: Isabelle_System,
40.44 + initial_font_size: Int,
40.45 + handler: PartialFunction[HTML_Panel.Event, Unit]) extends HtmlPanel
40.46 +{
40.47 + // global logging
40.48 + Logger.getLogger("org.lobobrowser").setLevel(Level.WARNING)
40.49 +
40.50 +
40.51 + /* document template */
40.52 +
40.53 + private def try_file(name: String): String =
40.54 + {
40.55 + val file = sys.platform_file(name)
40.56 + if (file.isFile) Source.fromFile(file).mkString else ""
40.57 + }
40.58 +
40.59 + private def template(font_size: Int): String =
40.60 + """<?xml version="1.0" encoding="utf-8"?>
40.61 +<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
40.62 + "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
40.63 +<html xmlns="http://www.w3.org/1999/xhtml">
40.64 +<head>
40.65 +<style media="all" type="text/css">
40.66 +""" +
40.67 + try_file("$ISABELLE_HOME/lib/html/isabelle.css") + "\n" +
40.68 + try_file("$ISABELLE_HOME_USER/etc/isabelle.css") + "\n" +
40.69 + "body { font-family: " + sys.font_family + "; font-size: " + font_size + "px }" +
40.70 +"""
40.71 +</style>
40.72 +</head>
40.73 +<body/>
40.74 +</html>
40.75 +"""
40.76 +
40.77 +
40.78 + /* actor with local state */
40.79 +
40.80 + private val ucontext = new SimpleUserAgentContext
40.81 +
40.82 + private val rcontext = new SimpleHtmlRendererContext(this, ucontext)
40.83 + {
40.84 + private def handle(event: HTML_Panel.Event): Boolean =
40.85 + if (handler != null && handler.isDefinedAt(event)) { handler(event); true }
40.86 + else false
40.87 +
40.88 + override def onContextMenu(elem: HTMLElement, event: MouseEvent): Boolean =
40.89 + handle(HTML_Panel.Context_Menu(elem, event))
40.90 + override def onMouseClick(elem: HTMLElement, event: MouseEvent): Boolean =
40.91 + handle(HTML_Panel.Mouse_Click(elem, event))
40.92 + override def onDoubleClick(elem: HTMLElement, event: MouseEvent): Boolean =
40.93 + handle(HTML_Panel.Double_Click(elem, event))
40.94 + override def onMouseOver(elem: HTMLElement, event: MouseEvent)
40.95 + { handle(HTML_Panel.Mouse_Over(elem, event)) }
40.96 + override def onMouseOut(elem: HTMLElement, event: MouseEvent)
40.97 + { handle(HTML_Panel.Mouse_Out(elem, event)) }
40.98 + }
40.99 +
40.100 + private val builder = new DocumentBuilderImpl(ucontext, rcontext)
40.101 +
40.102 + private case class Init(font_size: Int)
40.103 + private case class Render(body: List[XML.Tree])
40.104 +
40.105 + private val main_actor = actor {
40.106 + // crude double buffering
40.107 + var doc1: org.w3c.dom.Document = null
40.108 + var doc2: org.w3c.dom.Document = null
40.109 +
40.110 + loop {
40.111 + react {
40.112 + case Init(font_size) =>
40.113 + val src = template(font_size)
40.114 + def parse() =
40.115 + builder.parse(new InputSourceImpl(new StringReader(src), "http://localhost"))
40.116 + doc1 = parse()
40.117 + doc2 = parse()
40.118 + Swing_Thread.now { setDocument(doc1, rcontext) }
40.119 +
40.120 + case Render(body) =>
40.121 + val doc = doc2
40.122 + val node =
40.123 + XML.document_node(doc,
40.124 + XML.elem(HTML.BODY, body.map((t: XML.Tree) => XML.elem(HTML.PRE, HTML.spans(t)))))
40.125 + doc.removeChild(doc.getLastChild())
40.126 + doc.appendChild(node)
40.127 + doc2 = doc1
40.128 + doc1 = doc
40.129 + Swing_Thread.now { setDocument(doc1, rcontext) }
40.130 +
40.131 + case bad => System.err.println("main_actor: ignoring bad message " + bad)
40.132 + }
40.133 + }
40.134 + }
40.135 +
40.136 + main_actor ! Init(initial_font_size)
40.137 +
40.138 +
40.139 + /* main method wrappers */
40.140 +
40.141 + def init(font_size: Int) { main_actor ! Init(font_size) }
40.142 + def render(body: List[XML.Tree]) { main_actor ! Render(body) }
40.143 +}
41.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
41.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_encoding.scala Mon Jan 11 23:11:31 2010 +0100
41.3 @@ -0,0 +1,64 @@
41.4 +/*
41.5 + * Isabelle encoding -- based on utf-8
41.6 + *
41.7 + * @author Makarius
41.8 + */
41.9 +
41.10 +package isabelle.jedit
41.11 +
41.12 +
41.13 +import org.gjt.sp.jedit.io.Encoding
41.14 +import org.gjt.sp.jedit.buffer.JEditBuffer
41.15 +
41.16 +import java.nio.charset.{Charset, CharsetDecoder, CodingErrorAction}
41.17 +import java.io.{InputStream, OutputStream, Reader, Writer, InputStreamReader, OutputStreamWriter,
41.18 + CharArrayReader, ByteArrayOutputStream}
41.19 +
41.20 +import scala.io.{Source, BufferedSource}
41.21 +
41.22 +
41.23 +object Isabelle_Encoding
41.24 +{
41.25 + val NAME = "UTF-8-Isabelle"
41.26 +
41.27 + def is_active(buffer: JEditBuffer): Boolean =
41.28 + buffer.getStringProperty(JEditBuffer.ENCODING).asInstanceOf[String] == NAME
41.29 +}
41.30 +
41.31 +class Isabelle_Encoding extends Encoding
41.32 +{
41.33 + private val charset = Charset.forName(Standard_System.charset)
41.34 + private val BUFSIZE = 32768
41.35 +
41.36 + private def text_reader(in: InputStream, decoder: CharsetDecoder): Reader =
41.37 + {
41.38 + def source(): Source =
41.39 + BufferedSource.fromInputStream(in, decoder, BUFSIZE, { () => source() })
41.40 + new CharArrayReader(Isabelle.system.symbols.decode(source.mkString).toArray)
41.41 + }
41.42 +
41.43 + override def getTextReader(in: InputStream): Reader =
41.44 + text_reader(in, charset.newDecoder())
41.45 +
41.46 + override def getPermissiveTextReader(in: InputStream): Reader =
41.47 + {
41.48 + val decoder = charset.newDecoder()
41.49 + decoder.onMalformedInput(CodingErrorAction.REPLACE)
41.50 + decoder.onUnmappableCharacter(CodingErrorAction.REPLACE)
41.51 + text_reader(in, decoder)
41.52 + }
41.53 +
41.54 + override def getTextWriter(out: OutputStream): Writer =
41.55 + {
41.56 + val buffer = new ByteArrayOutputStream(BUFSIZE) {
41.57 + override def flush()
41.58 + {
41.59 + val text = Isabelle.system.symbols.encode(toString(Standard_System.charset))
41.60 + out.write(text.getBytes(Standard_System.charset))
41.61 + out.flush()
41.62 + }
41.63 + override def close() { out.close() }
41.64 + }
41.65 + new OutputStreamWriter(buffer, charset.newEncoder())
41.66 + }
41.67 +}
42.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
42.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Mon Jan 11 23:11:31 2010 +0100
42.3 @@ -0,0 +1,75 @@
42.4 +/*
42.5 + * Hyperlink setup for Isabelle proof documents
42.6 + *
42.7 + * @author Fabian Immler, TU Munich
42.8 + */
42.9 +
42.10 +package isabelle.jedit
42.11 +
42.12 +
42.13 +import java.io.File
42.14 +
42.15 +import gatchan.jedit.hyperlinks.{Hyperlink, HyperlinkSource, AbstractHyperlink}
42.16 +
42.17 +import org.gjt.sp.jedit.{View, jEdit, Buffer, TextUtilities}
42.18 +
42.19 +
42.20 +private class Internal_Hyperlink(start: Int, end: Int, line: Int, ref_offset: Int)
42.21 + extends AbstractHyperlink(start, end, line, "")
42.22 +{
42.23 + override def click(view: View) {
42.24 + view.getTextArea.moveCaretPosition(ref_offset)
42.25 + }
42.26 +}
42.27 +
42.28 +class External_Hyperlink(start: Int, end: Int, line: Int, ref_file: String, ref_line: Int)
42.29 + extends AbstractHyperlink(start, end, line, "")
42.30 +{
42.31 + override def click(view: View) = {
42.32 + Isabelle.system.source_file(ref_file) match {
42.33 + case None => System.err.println("Could not find source file " + ref_file) // FIXME ??
42.34 + case Some(file) =>
42.35 + jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + ref_line))
42.36 + }
42.37 + }
42.38 +}
42.39 +
42.40 +class Isabelle_Hyperlinks extends HyperlinkSource
42.41 +{
42.42 + def getHyperlink(buffer: Buffer, original_offset: Int): Hyperlink =
42.43 + {
42.44 + Document_Model(buffer) match {
42.45 + case Some(model) =>
42.46 + val document = model.recent_document()
42.47 + val offset = model.from_current(document, original_offset)
42.48 + document.command_at(offset) match {
42.49 + case Some((command, command_start)) =>
42.50 + document.current_state(command).get.ref_at(offset - command_start) match {
42.51 + case Some(ref) =>
42.52 + val begin = model.to_current(document, command_start + ref.start)
42.53 + val line = buffer.getLineOfOffset(begin)
42.54 + val end = model.to_current(document, command_start + ref.stop)
42.55 + ref.info match {
42.56 + case Command.RefInfo(Some(ref_file), Some(ref_line), _, _) =>
42.57 + new External_Hyperlink(begin, end, line, ref_file, ref_line)
42.58 + case Command.RefInfo(_, _, Some(id), Some(offset)) =>
42.59 + Isabelle.session.lookup_entity(id) match {
42.60 + case Some(ref_cmd: Command) =>
42.61 + document.command_start(ref_cmd) match {
42.62 + case Some(ref_cmd_start) =>
42.63 + new Internal_Hyperlink(begin, end, line,
42.64 + model.to_current(document, ref_cmd_start + offset - 1))
42.65 + case None => null // FIXME external ref
42.66 + }
42.67 + case _ => null
42.68 + }
42.69 + case _ => null
42.70 + }
42.71 + case None => null
42.72 + }
42.73 + case None => null
42.74 + }
42.75 + case None => null
42.76 + }
42.77 + }
42.78 +}
43.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
43.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_options.scala Mon Jan 11 23:11:31 2010 +0100
43.3 @@ -0,0 +1,53 @@
43.4 +/*
43.5 + * Editor pane for plugin options
43.6 + *
43.7 + * @author Johannes Hölzl, TU Munich
43.8 + */
43.9 +
43.10 +package isabelle.jedit
43.11 +
43.12 +
43.13 +import javax.swing.{JComboBox, JSpinner}
43.14 +
43.15 +import org.gjt.sp.jedit.AbstractOptionPane
43.16 +
43.17 +
43.18 +class Isabelle_Options extends AbstractOptionPane("isabelle")
43.19 +{
43.20 + private val logic_name = new JComboBox()
43.21 + private val font_size = new JSpinner()
43.22 +
43.23 + private class List_Item(val name: String, val descr: String) {
43.24 + def this(name: String) = this(name, name)
43.25 + override def toString = descr
43.26 + }
43.27 +
43.28 + override def _init()
43.29 + {
43.30 + val logic = Isabelle.Property("logic")
43.31 + addComponent(Isabelle.Property("logic.title"), {
43.32 + logic_name.addItem(new List_Item("", "default (" + Isabelle.default_logic() + ")"))
43.33 + for (name <- Isabelle.system.find_logics()) {
43.34 + val item = new List_Item(name)
43.35 + logic_name.addItem(item)
43.36 + if (name == logic)
43.37 + logic_name.setSelectedItem(item)
43.38 + }
43.39 + logic_name
43.40 + })
43.41 +
43.42 + addComponent(Isabelle.Property("font-size.title"), {
43.43 + font_size.setValue(Isabelle.Int_Property("font-size"))
43.44 + font_size
43.45 + })
43.46 + }
43.47 +
43.48 + override def _save()
43.49 + {
43.50 + val logic = logic_name.getSelectedItem.asInstanceOf[List_Item].name
43.51 + Isabelle.Property("logic") = logic
43.52 +
43.53 + val size = font_size.getValue().asInstanceOf[Int]
43.54 + Isabelle.Int_Property("font-size") = size
43.55 + }
43.56 +}
44.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
44.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Mon Jan 11 23:11:31 2010 +0100
44.3 @@ -0,0 +1,98 @@
44.4 +/*
44.5 + * SideKick parser for Isabelle proof documents
44.6 + *
44.7 + * @author Fabian Immler, TU Munich
44.8 + * @author Makarius
44.9 + */
44.10 +
44.11 +package isabelle.jedit
44.12 +
44.13 +
44.14 +import scala.collection.Set
44.15 +import scala.collection.immutable.TreeSet
44.16 +
44.17 +import javax.swing.tree.DefaultMutableTreeNode
44.18 +import javax.swing.text.Position
44.19 +import javax.swing.Icon
44.20 +
44.21 +import org.gjt.sp.jedit.{Buffer, EditPane, TextUtilities, View}
44.22 +import errorlist.DefaultErrorSource
44.23 +import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, IAsset}
44.24 +
44.25 +
44.26 +class Isabelle_Sidekick extends SideKickParser("isabelle")
44.27 +{
44.28 + /* parsing */
44.29 +
44.30 + @volatile private var stopped = false
44.31 + override def stop() = { stopped = true }
44.32 +
44.33 + def parse(buffer: Buffer, error_source: DefaultErrorSource): SideKickParsedData =
44.34 + {
44.35 + implicit def int_to_pos(offset: Int): Position =
44.36 + new Position { def getOffset = offset; override def toString = offset.toString }
44.37 +
44.38 + stopped = false
44.39 +
44.40 + // FIXME lock buffer !??
44.41 + val data = new SideKickParsedData(buffer.getName)
44.42 + val root = data.root
44.43 + data.getAsset(root).setEnd(buffer.getLength)
44.44 +
44.45 + Swing_Thread.now { Document_Model(buffer) } match {
44.46 + case Some(model) =>
44.47 + val document = model.recent_document()
44.48 + for ((command, command_start) <- document.command_range(0) if !stopped) {
44.49 + root.add(document.current_state(command).get.markup_root.swing_tree((node: Markup_Node) =>
44.50 + {
44.51 + val content = command.source(node.start, node.stop)
44.52 + val id = command.id
44.53 +
44.54 + new DefaultMutableTreeNode(new IAsset {
44.55 + override def getIcon: Icon = null
44.56 + override def getShortString: String = content
44.57 + override def getLongString: String = node.info.toString
44.58 + override def getName: String = id
44.59 + override def setName(name: String) = ()
44.60 + override def setStart(start: Position) = ()
44.61 + override def getStart: Position = command_start + node.start
44.62 + override def setEnd(end: Position) = ()
44.63 + override def getEnd: Position = command_start + node.stop
44.64 + override def toString = id + ": " + content + "[" + getStart + " - " + getEnd + "]"
44.65 + })
44.66 + }))
44.67 + }
44.68 + if (stopped) root.add(new DefaultMutableTreeNode("<parser stopped>"))
44.69 + case None => root.add(new DefaultMutableTreeNode("<buffer inactive>"))
44.70 + }
44.71 + data
44.72 + }
44.73 +
44.74 +
44.75 + /* completion */
44.76 +
44.77 + override def supportsCompletion = true
44.78 + override def canCompleteAnywhere = true
44.79 +
44.80 + override def complete(pane: EditPane, caret: Int): SideKickCompletion =
44.81 + {
44.82 + val buffer = pane.getBuffer
44.83 +
44.84 + val line = buffer.getLineOfOffset(caret)
44.85 + val start = buffer.getLineStartOffset(line)
44.86 + val text = buffer.getSegment(start, caret - start)
44.87 +
44.88 + val completion = Isabelle.session.current_syntax.completion
44.89 +
44.90 + completion.complete(text) match {
44.91 + case None => null
44.92 + case Some((word, cs)) =>
44.93 + val ds =
44.94 + if (Isabelle_Encoding.is_active(buffer))
44.95 + cs.map(Isabelle.system.symbols.decode(_)).sort(_ < _)
44.96 + else cs
44.97 + new SideKickCompletion(pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { }
44.98 + }
44.99 + }
44.100 +
44.101 +}
45.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
45.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala Mon Jan 11 23:11:31 2010 +0100
45.3 @@ -0,0 +1,145 @@
45.4 +/*
45.5 + * include isabelle's command- and keyword-declarations
45.6 + * live in jEdits syntax-highlighting
45.7 + *
45.8 + * @author Fabian Immler, TU Munich
45.9 + */
45.10 +
45.11 +package isabelle.jedit
45.12 +
45.13 +
45.14 +import isabelle.Markup
45.15 +
45.16 +import org.gjt.sp.jedit.buffer.JEditBuffer
45.17 +import org.gjt.sp.jedit.syntax.{Token, TokenMarker, TokenHandler, SyntaxStyle, ParserRuleSet}
45.18 +
45.19 +import java.awt.Color
45.20 +import java.awt.Font
45.21 +import javax.swing.text.Segment;
45.22 +
45.23 +
45.24 +object Isabelle_Token_Marker
45.25 +{
45.26 + /* line context */
45.27 +
45.28 + private val rule_set = new ParserRuleSet("isabelle", "MAIN")
45.29 + private class LineContext(val line: Int, prev: LineContext)
45.30 + extends TokenMarker.LineContext(rule_set, prev)
45.31 +
45.32 +
45.33 + /* mapping to jEdit token types */
45.34 + // TODO: as properties or CSS style sheet
45.35 +
45.36 + private val choose_byte: Map[String, Byte] =
45.37 + {
45.38 + import Token._
45.39 + Map[String, Byte](
45.40 + // logical entities
45.41 + Markup.TCLASS -> LABEL,
45.42 + Markup.TYCON -> LABEL,
45.43 + Markup.FIXED_DECL -> LABEL,
45.44 + Markup.FIXED -> LABEL,
45.45 + Markup.CONST_DECL -> LABEL,
45.46 + Markup.CONST -> LABEL,
45.47 + Markup.FACT_DECL -> LABEL,
45.48 + Markup.FACT -> LABEL,
45.49 + Markup.DYNAMIC_FACT -> LABEL,
45.50 + Markup.LOCAL_FACT_DECL -> LABEL,
45.51 + Markup.LOCAL_FACT -> LABEL,
45.52 + // inner syntax
45.53 + Markup.TFREE -> LITERAL2,
45.54 + Markup.FREE -> LITERAL2,
45.55 + Markup.TVAR -> LITERAL3,
45.56 + Markup.SKOLEM -> LITERAL3,
45.57 + Markup.BOUND -> LITERAL3,
45.58 + Markup.VAR -> LITERAL3,
45.59 + Markup.NUM -> DIGIT,
45.60 + Markup.FLOAT -> DIGIT,
45.61 + Markup.XNUM -> DIGIT,
45.62 + Markup.XSTR -> LITERAL4,
45.63 + Markup.LITERAL -> LITERAL4,
45.64 + Markup.INNER_COMMENT -> COMMENT1,
45.65 + Markup.SORT -> FUNCTION,
45.66 + Markup.TYP -> FUNCTION,
45.67 + Markup.TERM -> FUNCTION,
45.68 + Markup.PROP -> FUNCTION,
45.69 + Markup.ATTRIBUTE -> FUNCTION,
45.70 + Markup.METHOD -> FUNCTION,
45.71 + // ML syntax
45.72 + Markup.ML_KEYWORD -> KEYWORD2,
45.73 + Markup.ML_IDENT -> NULL,
45.74 + Markup.ML_TVAR -> LITERAL3,
45.75 + Markup.ML_NUMERAL -> DIGIT,
45.76 + Markup.ML_CHAR -> LITERAL1,
45.77 + Markup.ML_STRING -> LITERAL1,
45.78 + Markup.ML_COMMENT -> COMMENT1,
45.79 + Markup.ML_MALFORMED -> INVALID,
45.80 + // embedded source text
45.81 + Markup.ML_SOURCE -> COMMENT4,
45.82 + Markup.DOC_SOURCE -> COMMENT4,
45.83 + Markup.ANTIQ -> COMMENT4,
45.84 + Markup.ML_ANTIQ -> COMMENT4,
45.85 + Markup.DOC_ANTIQ -> COMMENT4,
45.86 + // outer syntax
45.87 + Markup.IDENT -> NULL,
45.88 + Markup.COMMAND -> OPERATOR,
45.89 + Markup.KEYWORD -> KEYWORD4,
45.90 + Markup.VERBATIM -> COMMENT3,
45.91 + Markup.COMMENT -> COMMENT1,
45.92 + Markup.CONTROL -> COMMENT3,
45.93 + Markup.MALFORMED -> INVALID,
45.94 + Markup.STRING -> LITERAL3,
45.95 + Markup.ALTSTRING -> LITERAL1
45.96 + ).withDefaultValue(NULL)
45.97 + }
45.98 +
45.99 + def choose_color(kind: String, styles: Array[SyntaxStyle]): Color =
45.100 + styles(choose_byte(kind)).getForegroundColor
45.101 +}
45.102 +
45.103 +
45.104 +class Isabelle_Token_Marker(model: Document_Model) extends TokenMarker
45.105 +{
45.106 + override def markTokens(prev: TokenMarker.LineContext,
45.107 + handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext =
45.108 + {
45.109 + val previous = prev.asInstanceOf[Isabelle_Token_Marker.LineContext]
45.110 + val line = if (prev == null) 0 else previous.line + 1
45.111 + val context = new Isabelle_Token_Marker.LineContext(line, previous)
45.112 + val start = model.buffer.getLineStartOffset(line)
45.113 + val stop = start + line_segment.count
45.114 +
45.115 + val document = model.recent_document()
45.116 + def to: Int => Int = model.to_current(document, _)
45.117 + def from: Int => Int = model.from_current(document, _)
45.118 +
45.119 + var next_x = start
45.120 + for {
45.121 + (command, command_start) <- document.command_range(from(start), from(stop))
45.122 + markup <- document.current_state(command).get.highlight.flatten
45.123 + val abs_start = to(command_start + markup.start)
45.124 + val abs_stop = to(command_start + markup.stop)
45.125 + if (abs_stop > start)
45.126 + if (abs_start < stop)
45.127 + val byte = Isabelle_Token_Marker.choose_byte(markup.info.toString)
45.128 + val token_start = (abs_start - start) max 0
45.129 + val token_length =
45.130 + (abs_stop - abs_start) -
45.131 + ((start - abs_start) max 0) -
45.132 + ((abs_stop - stop) max 0)
45.133 + }
45.134 + {
45.135 + if (start + token_start > next_x)
45.136 + handler.handleToken(line_segment, 1,
45.137 + next_x - start, start + token_start - next_x, context)
45.138 + handler.handleToken(line_segment, byte, token_start, token_length, context)
45.139 + next_x = start + token_start + token_length
45.140 + }
45.141 + if (next_x < stop)
45.142 + handler.handleToken(line_segment, 1, next_x - start, stop - next_x, context)
45.143 +
45.144 + handler.handleToken(line_segment, Token.END, line_segment.count, 0, context)
45.145 + handler.setLineContext(context)
45.146 + context
45.147 + }
45.148 +}
46.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
46.2 +++ b/src/Tools/jEdit/src/jedit/output_dockable.scala Mon Jan 11 23:11:31 2010 +0100
46.3 @@ -0,0 +1,64 @@
46.4 +/*
46.5 + * Dockable window with result message output
46.6 + *
46.7 + * @author Makarius
46.8 + */
46.9 +
46.10 +package isabelle.jedit
46.11 +
46.12 +
46.13 +import scala.actors.Actor._
46.14 +
46.15 +import javax.swing.JPanel
46.16 +import java.awt.{BorderLayout, Dimension}
46.17 +
46.18 +import org.gjt.sp.jedit.View
46.19 +import org.gjt.sp.jedit.gui.DockableWindowManager
46.20 +
46.21 +
46.22 +
46.23 +class Output_Dockable(view: View, position: String) extends JPanel(new BorderLayout)
46.24 +{
46.25 + if (position == DockableWindowManager.FLOATING)
46.26 + setPreferredSize(new Dimension(500, 250))
46.27 +
46.28 + private val html_panel =
46.29 + new HTML_Panel(Isabelle.system, Isabelle.Int_Property("font-size"), null)
46.30 + add(html_panel, BorderLayout.CENTER)
46.31 +
46.32 +
46.33 + /* actor wiring */
46.34 +
46.35 + private val output_actor = actor {
46.36 + loop {
46.37 + react {
46.38 + case cmd: Command =>
46.39 + Swing_Thread.now { Document_Model(view.getBuffer) } match {
46.40 + case None =>
46.41 + case Some(model) =>
46.42 + val body = model.recent_document.current_state(cmd).map(_.results) getOrElse Nil
46.43 + html_panel.render(body)
46.44 + }
46.45 +
46.46 + case Session.Global_Settings =>
46.47 + html_panel.init(Isabelle.Int_Property("font-size"))
46.48 +
46.49 + case bad => System.err.println("output_actor: ignoring bad message " + bad)
46.50 + }
46.51 + }
46.52 + }
46.53 +
46.54 + override def addNotify()
46.55 + {
46.56 + super.addNotify()
46.57 + Isabelle.session.results += output_actor
46.58 + Isabelle.session.global_settings += output_actor
46.59 + }
46.60 +
46.61 + override def removeNotify()
46.62 + {
46.63 + Isabelle.session.results -= output_actor
46.64 + Isabelle.session.global_settings -= output_actor
46.65 + super.removeNotify()
46.66 + }
46.67 +}
47.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
47.2 +++ b/src/Tools/jEdit/src/jedit/plugin.scala Mon Jan 11 23:11:31 2010 +0100
47.3 @@ -0,0 +1,195 @@
47.4 +/*
47.5 + * Main Isabelle/jEdit plugin setup
47.6 + *
47.7 + * @author Johannes Hölzl, TU Munich
47.8 + * @author Fabian Immler, TU Munich
47.9 + * @author Makarius
47.10 + */
47.11 +
47.12 +package isabelle.jedit
47.13 +
47.14 +
47.15 +import java.io.{FileInputStream, IOException}
47.16 +import java.awt.Font
47.17 +import javax.swing.JTextArea
47.18 +
47.19 +import scala.collection.mutable
47.20 +
47.21 +import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, EditPane, ServiceManager, View}
47.22 +import org.gjt.sp.jedit.buffer.JEditBuffer
47.23 +import org.gjt.sp.jedit.textarea.JEditTextArea
47.24 +import org.gjt.sp.jedit.msg.{EditPaneUpdate, PropertiesChanged}
47.25 +
47.26 +
47.27 +object Isabelle
47.28 +{
47.29 + /* plugin instance */
47.30 +
47.31 + var system: Isabelle_System = null
47.32 + var session: Session = null
47.33 +
47.34 +
47.35 + /* name */
47.36 +
47.37 + val NAME = "Isabelle"
47.38 +
47.39 +
47.40 + /* properties */
47.41 +
47.42 + val OPTION_PREFIX = "options.isabelle."
47.43 +
47.44 + object Property
47.45 + {
47.46 + def apply(name: String): String = jEdit.getProperty(OPTION_PREFIX + name)
47.47 + def update(name: String, value: String) = jEdit.setProperty(OPTION_PREFIX + name, value)
47.48 + }
47.49 +
47.50 + object Boolean_Property
47.51 + {
47.52 + def apply(name: String): Boolean = jEdit.getBooleanProperty(OPTION_PREFIX + name)
47.53 + def update(name: String, value: Boolean) = jEdit.setBooleanProperty(OPTION_PREFIX + name, value)
47.54 + }
47.55 +
47.56 + object Int_Property
47.57 + {
47.58 + def apply(name: String): Int = jEdit.getIntegerProperty(OPTION_PREFIX + name)
47.59 + def update(name: String, value: Int) = jEdit.setIntegerProperty(OPTION_PREFIX + name, value)
47.60 + }
47.61 +
47.62 +
47.63 + /* settings */
47.64 +
47.65 + def default_logic(): String =
47.66 + {
47.67 + val logic = system.getenv("JEDIT_LOGIC")
47.68 + if (logic != "") logic
47.69 + else system.getenv_strict("ISABELLE_LOGIC")
47.70 + }
47.71 +
47.72 + def isabelle_args(): List[String] =
47.73 + {
47.74 + val modes = system.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _)
47.75 + val logic = {
47.76 + val logic = Property("logic")
47.77 + if (logic != null && logic != "") logic
47.78 + else default_logic()
47.79 + }
47.80 + modes ++ List(logic)
47.81 + }
47.82 +
47.83 +
47.84 + /* main jEdit components */ // FIXME ownership!?
47.85 +
47.86 + def jedit_buffers(): Iterator[Buffer] = Iterator.fromArray(jEdit.getBuffers())
47.87 +
47.88 + def jedit_views(): Iterator[View] = Iterator.fromArray(jEdit.getViews())
47.89 +
47.90 + def jedit_text_areas(view: View): Iterator[JEditTextArea] =
47.91 + Iterator.fromArray(view.getEditPanes).map(_.getTextArea)
47.92 +
47.93 + def jedit_text_areas(): Iterator[JEditTextArea] =
47.94 + jedit_views().flatMap(jedit_text_areas(_))
47.95 +
47.96 + def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] =
47.97 + jedit_text_areas().filter(_.getBuffer == buffer)
47.98 +
47.99 +
47.100 + /* manage prover */
47.101 +
47.102 + private def prover_started(view: View): Boolean =
47.103 + {
47.104 + val timeout = Int_Property("startup-timeout") max 1000
47.105 + session.start(timeout, Isabelle.isabelle_args()) match {
47.106 + case Some(err) =>
47.107 + val text = new JTextArea(err); text.setEditable(false)
47.108 + Library.error_dialog(view, null, "Failed to start Isabelle process", text)
47.109 + false
47.110 + case None => true
47.111 + }
47.112 + }
47.113 +
47.114 +
47.115 + /* activation */
47.116 +
47.117 + def activate_buffer(view: View, buffer: Buffer)
47.118 + {
47.119 + if (prover_started(view)) {
47.120 + val model = Document_Model.init(session, buffer)
47.121 + for (text_area <- jedit_text_areas(buffer))
47.122 + Document_View.init(model, text_area)
47.123 + }
47.124 + }
47.125 +
47.126 + def deactivate_buffer(buffer: Buffer)
47.127 + {
47.128 + session.stop() // FIXME not yet
47.129 +
47.130 + for (text_area <- jedit_text_areas(buffer))
47.131 + Document_View.exit(text_area)
47.132 + Document_Model.exit(buffer)
47.133 + }
47.134 +
47.135 + def switch_active(view: View) =
47.136 + {
47.137 + val buffer = view.getBuffer
47.138 + if (Document_Model(buffer).isDefined) deactivate_buffer(buffer)
47.139 + else activate_buffer(view, buffer)
47.140 + }
47.141 +
47.142 + def is_active(view: View): Boolean =
47.143 + Document_Model(view.getBuffer).isDefined
47.144 +}
47.145 +
47.146 +
47.147 +class Plugin extends EBPlugin
47.148 +{
47.149 + /* main plugin plumbing */
47.150 +
47.151 + override def handleMessage(message: EBMessage)
47.152 + {
47.153 + message match {
47.154 + case msg: EditPaneUpdate =>
47.155 + val edit_pane = msg.getEditPane
47.156 + val buffer = edit_pane.getBuffer
47.157 + val text_area = edit_pane.getTextArea
47.158 +
47.159 + def init_view()
47.160 + {
47.161 + Document_Model(buffer) match {
47.162 + case Some(model) => Document_View.init(model, text_area)
47.163 + case None =>
47.164 + }
47.165 + }
47.166 + def exit_view()
47.167 + {
47.168 + if (Document_View(text_area).isDefined)
47.169 + Document_View.exit(text_area)
47.170 + }
47.171 + msg.getWhat match {
47.172 + case EditPaneUpdate.BUFFER_CHANGED => exit_view(); init_view()
47.173 + case EditPaneUpdate.CREATED => init_view()
47.174 + case EditPaneUpdate.DESTROYED => exit_view()
47.175 + case _ =>
47.176 + }
47.177 +
47.178 + case msg: PropertiesChanged =>
47.179 + Isabelle.session.global_settings.event(Session.Global_Settings)
47.180 +
47.181 + case _ =>
47.182 + }
47.183 + }
47.184 +
47.185 + override def start()
47.186 + {
47.187 + Isabelle.system = new Isabelle_System
47.188 + Isabelle.system.install_fonts()
47.189 + Isabelle.session = new Session(Isabelle.system) // FIXME dialog!?
47.190 + }
47.191 +
47.192 + override def stop()
47.193 + {
47.194 + Isabelle.session.stop() // FIXME dialog!?
47.195 + Isabelle.session = null
47.196 + Isabelle.system = null
47.197 + }
47.198 +}
48.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
48.2 +++ b/src/Tools/jEdit/src/jedit/protocol_dockable.scala Mon Jan 11 23:11:31 2010 +0100
48.3 @@ -0,0 +1,52 @@
48.4 +/*
48.5 + * Dockable window for raw process output
48.6 + *
48.7 + * @author Makarius
48.8 + */
48.9 +
48.10 +package isabelle.jedit
48.11 +
48.12 +
48.13 +import scala.actors.Actor._
48.14 +
48.15 +import java.awt.{Dimension, Graphics, BorderLayout}
48.16 +import javax.swing.{JPanel, JTextArea, JScrollPane}
48.17 +
48.18 +import org.gjt.sp.jedit.View
48.19 +import org.gjt.sp.jedit.gui.DockableWindowManager
48.20 +
48.21 +
48.22 +class Protocol_Dockable(view: View, position: String) extends JPanel(new BorderLayout)
48.23 +{
48.24 + if (position == DockableWindowManager.FLOATING)
48.25 + setPreferredSize(new Dimension(500, 250))
48.26 +
48.27 + private val text_area = new JTextArea
48.28 + add(new JScrollPane(text_area), BorderLayout.CENTER)
48.29 +
48.30 +
48.31 + /* actor wiring */
48.32 +
48.33 + private val raw_actor = actor {
48.34 + loop {
48.35 + react {
48.36 + case result: Isabelle_Process.Result =>
48.37 + Swing_Thread.now { text_area.append(result.toString + "\n") }
48.38 +
48.39 + case bad => System.err.println("raw_actor: ignoring bad message " + bad)
48.40 + }
48.41 + }
48.42 + }
48.43 +
48.44 + override def addNotify()
48.45 + {
48.46 + super.addNotify()
48.47 + Isabelle.session.raw_results += raw_actor
48.48 + }
48.49 +
48.50 + override def removeNotify()
48.51 + {
48.52 + Isabelle.session.raw_results -= raw_actor
48.53 + super.removeNotify()
48.54 + }
48.55 +}
49.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
49.2 +++ b/src/Tools/jEdit/src/jedit/scala_console.scala Mon Jan 11 23:11:31 2010 +0100
49.3 @@ -0,0 +1,153 @@
49.4 +/*
49.5 + * Scala instance of Console plugin
49.6 + *
49.7 + * @author Makarius
49.8 + */
49.9 +
49.10 +package isabelle.jedit
49.11 +
49.12 +
49.13 +import console.{Console, ConsolePane, Shell, Output}
49.14 +
49.15 +import org.gjt.sp.jedit.{jEdit, JARClassLoader}
49.16 +import org.gjt.sp.jedit.MiscUtilities
49.17 +
49.18 +import java.io.{File, OutputStream, Writer, PrintWriter}
49.19 +
49.20 +import scala.tools.nsc.{Interpreter, GenericRunnerSettings, NewLinePrintWriter, ConsoleWriter}
49.21 +import scala.collection.mutable
49.22 +
49.23 +
49.24 +class Scala_Console extends Shell("Scala")
49.25 +{
49.26 + /* reconstructed jEdit/plugin classpath */
49.27 +
49.28 + private def reconstruct_classpath(): String =
49.29 + {
49.30 + def find_jars(start: String): List[String] =
49.31 + if (start != null)
49.32 + Standard_System.find_files(new File(start),
49.33 + entry => entry.isFile && entry.getName.endsWith(".jar")).map(_.getAbsolutePath)
49.34 + else Nil
49.35 + val path = find_jars(jEdit.getSettingsDirectory) ::: find_jars(jEdit.getJEditHome)
49.36 + path.mkString(File.pathSeparator)
49.37 + }
49.38 +
49.39 +
49.40 + /* global state -- owned by Swing thread */
49.41 +
49.42 + private var interpreters = Map[Console, Interpreter]()
49.43 +
49.44 + private var global_console: Console = null
49.45 + private var global_out: Output = null
49.46 + private var global_err: Output = null
49.47 +
49.48 + private val console_stream = new OutputStream
49.49 + {
49.50 + val buf = new StringBuilder
49.51 + override def flush()
49.52 + {
49.53 + val str = Standard_System.decode_permissive_utf8(buf.toString)
49.54 + buf.clear
49.55 + if (global_out == null) System.out.print(str)
49.56 + else Swing_Thread.now { global_out.writeAttrs(null, str) }
49.57 + }
49.58 + override def close() { flush () }
49.59 + def write(byte: Int) { buf.append(byte.toChar) }
49.60 + }
49.61 +
49.62 + private val console_writer = new Writer
49.63 + {
49.64 + def flush() {}
49.65 + def close() {}
49.66 +
49.67 + def write(cbuf: Array[Char], off: Int, len: Int)
49.68 + {
49.69 + if (len > 0) write(new String(cbuf.subArray(off, off + len)))
49.70 + }
49.71 +
49.72 + override def write(str: String)
49.73 + {
49.74 + if (global_out == null) System.out.println(str)
49.75 + else global_out.print(null, str)
49.76 + }
49.77 + }
49.78 +
49.79 + private def with_console[A](console: Console, out: Output, err: Output)(e: => A): A =
49.80 + {
49.81 + global_console = console
49.82 + global_out = out
49.83 + global_err = if (err == null) out else err
49.84 + val res = Exn.capture { scala.Console.withOut(console_stream)(e) }
49.85 + console_stream.flush
49.86 + global_console = null
49.87 + global_out = null
49.88 + global_err = null
49.89 + Exn.release(res)
49.90 + }
49.91 +
49.92 + private def report_error(str: String)
49.93 + {
49.94 + if (global_console == null || global_err == null) System.err.println(str)
49.95 + else Swing_Thread.now { global_err.print(global_console.getErrorColor, str) }
49.96 + }
49.97 +
49.98 +
49.99 + /* jEdit console methods */
49.100 +
49.101 + override def openConsole(console: Console)
49.102 + {
49.103 + val settings = new GenericRunnerSettings(report_error)
49.104 + settings.classpath.value = reconstruct_classpath()
49.105 +
49.106 + val interp = new Interpreter(settings, new PrintWriter(console_writer, true))
49.107 + {
49.108 + override def parentClassLoader = new JARClassLoader
49.109 + }
49.110 + interp.setContextClassLoader
49.111 + interp.bind("view", "org.gjt.sp.jedit.View", console.getView)
49.112 + interp.bind("console", "console.Console", console)
49.113 + interp.interpret("import isabelle.jedit.Isabelle")
49.114 +
49.115 + interpreters += (console -> interp)
49.116 + }
49.117 +
49.118 + override def closeConsole(console: Console)
49.119 + {
49.120 + interpreters -= console
49.121 + }
49.122 +
49.123 + override def printInfoMessage(out: Output)
49.124 + {
49.125 + out.print(null,
49.126 + "This shell evaluates Isabelle/Scala expressions.\n\n" +
49.127 + "The following special toplevel bindings are provided:\n" +
49.128 + " view -- current jEdit/Swing view (e.g. view.getBuffer, view.getTextArea)\n" +
49.129 + " console -- jEdit Console plugin instance\n" +
49.130 + " Isabelle -- Isabelle plugin instance (e.g. Isabelle.system, Isabelle.session)\n")
49.131 + }
49.132 +
49.133 + override def printPrompt(console: Console, out: Output)
49.134 + {
49.135 + out.writeAttrs(ConsolePane.colorAttributes(console.getInfoColor), "scala>")
49.136 + out.writeAttrs(ConsolePane.colorAttributes(console.getPlainColor), " ")
49.137 + }
49.138 +
49.139 + override def execute(console: Console, input: String, out: Output, err: Output, command: String)
49.140 + {
49.141 + val interp = interpreters(console)
49.142 + with_console(console, out, err) { interp.interpret(command) }
49.143 + if (err != null) err.commandDone()
49.144 + out.commandDone()
49.145 + }
49.146 +
49.147 + override def stop(console: Console)
49.148 + {
49.149 + closeConsole(console)
49.150 + console.clear
49.151 + openConsole(console)
49.152 + val out = console.getOutput
49.153 + out.commandDone
49.154 + printPrompt(console, out)
49.155 + }
49.156 +}