--- a/Admin/component_repository/components.sha1 Mon Sep 03 18:12:59 2012 +0200
+++ b/Admin/component_repository/components.sha1 Mon Sep 03 22:51:33 2012 +0200
@@ -11,6 +11,7 @@
ed72630f307729df08fdedb095f0af8725f81b9c jedit_build-20120327.tar.gz
6425f622625024c1de27f3730d6811f6370a19cd jedit_build-20120414.tar.gz
7b012f725ec1cc102dc259df178d511cc7890bba jedit_build-20120813.tar.gz
+70928b6dc49c38599e7310a532ee924c367d7440 jedit_build-20120903.tar.gz
6c737137cc597fc920943783382e928ea79e3feb kodkodi-1.2.16.tar.gz
1c8cb6a8f4cbeaedce2d6d1ba8fc7e2ab3663aeb polyml-5.4.1.tar.gz
8ee375cfc38972f080dbc78f07b68dac03efe968 ProofGeneral-3.7.1.1.tar.gz
--- a/Admin/components/main Mon Sep 03 18:12:59 2012 +0200
+++ b/Admin/components/main Mon Sep 03 22:51:33 2012 +0200
@@ -2,7 +2,7 @@
cvc3-2.4.1
e-1.5
jdk-7u6
-jedit_build-20120813
+jedit_build-20120903
kodkodi-1.2.16
polyml-5.4.1
scala-2.9.2
--- a/src/Pure/System/build.scala Mon Sep 03 18:12:59 2012 +0200
+++ b/src/Pure/System/build.scala Mon Sep 03 22:51:33 2012 +0200
@@ -331,7 +331,8 @@
def sources(name: String): List[SHA1.Digest] = deps(name).sources.map(_._2)
}
- def dependencies(verbose: Boolean, list_files: Boolean, tree: Session_Tree): Deps =
+ def dependencies(inlined_files: Boolean, verbose: Boolean, list_files: Boolean,
+ tree: Session_Tree): Deps =
Deps((Map.empty[String, Session_Content] /: tree.topological_order)(
{ case (deps, (name, info)) =>
val (preloaded, parent_syntax, parent_errors) =
@@ -352,7 +353,7 @@
}
val thy_deps =
- thy_info.dependencies(
+ thy_info.dependencies(inlined_files,
info.theories.map(_._2).flatten.
map(thy => Document.Node.Name(info.dir + Thy_Load.thy_path(thy))))
@@ -381,15 +382,15 @@
deps + (name -> Session_Content(loaded_theories, syntax, sources, errors))
}))
- def session_content(dirs: List[Path], session: String): Session_Content =
+ def session_content(inlined_files: Boolean, dirs: List[Path], session: String): Session_Content =
{
val (_, tree) =
find_sessions(Options.init(), dirs.map((false, _))).required(false, Nil, List(session))
- dependencies(false, false, tree)(session)
+ dependencies(inlined_files, false, false, tree)(session)
}
def outer_syntax(session: String): Outer_Syntax =
- session_content(Nil, session).check_errors.syntax
+ session_content(false, Nil, session).check_errors.syntax
/* jobs */
@@ -548,7 +549,7 @@
val options = (Options.init() /: build_options)(_ + _)
val (descendants, tree) =
find_sessions(options, more_dirs).required(all_sessions, session_groups, sessions)
- val deps = dependencies(verbose, list_files, tree)
+ val deps = dependencies(true, verbose, list_files, tree)
val queue = Queue(tree)
def make_stamp(name: String): String =
--- a/src/Pure/Thy/thy_info.scala Mon Sep 03 18:12:59 2012 +0200
+++ b/src/Pure/Thy/thy_info.scala Mon Sep 03 22:51:33 2012 +0200
@@ -50,11 +50,11 @@
def make_syntax: Outer_Syntax = thy_load.base_syntax.add_keywords(keywords)
}
- private def require_thys(initiators: List[Document.Node.Name],
+ private def require_thys(files: Boolean, initiators: List[Document.Node.Name],
required: Dependencies, names: List[Document.Node.Name]): Dependencies =
- (required /: names)(require_thy(initiators, _, _))
+ (required /: names)(require_thy(files, initiators, _, _))
- private def require_thy(initiators: List[Document.Node.Name],
+ private def require_thy(files: Boolean, initiators: List[Document.Node.Name],
required: Dependencies, name: Document.Node.Name): Dependencies =
{
if (required.seen(name)) required
@@ -64,13 +64,16 @@
if (initiators.contains(name)) error(cycle_msg(initiators))
val syntax = required.make_syntax
val header =
- try { thy_load.check_thy_files(syntax, name) }
+ try {
+ if (files) thy_load.check_thy_files(syntax, name)
+ else thy_load.check_thy(name)
+ }
catch {
case ERROR(msg) =>
cat_error(msg, "The error(s) above occurred while examining theory " +
quote(name.theory) + required_by(initiators))
}
- (name, header) :: require_thys(name :: initiators, required + name, header.imports)
+ (name, header) :: require_thys(files, name :: initiators, required + name, header.imports)
}
catch {
case e: Throwable =>
@@ -79,6 +82,6 @@
}
}
- def dependencies(names: List[Document.Node.Name]): Dependencies =
- require_thys(Nil, Dependencies.empty, names)
+ def dependencies(inlined_files: Boolean, names: List[Document.Node.Name]): Dependencies =
+ require_thys(inlined_files, Nil, Dependencies.empty, names)
}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/jedit-4.5.2/chunks Mon Sep 03 22:51:33 2012 +0200
@@ -0,0 +1,16 @@
+diff -ru jEdit/org/gjt/sp/jedit/textarea/TextArea.java jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java
+--- jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2012-08-13 19:11:04.000000000 +0200
++++ jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java 2012-09-03 19:37:48.000000000 +0200
+@@ -905,6 +905,11 @@
+ return chunkCache.getLineInfo(screenLine).physicalLine;
+ } //}}}
+
++ public Chunk getChunksOfScreenLine(int screenLine)
++ {
++ return chunkCache.getLineInfo(screenLine).chunks;
++ }
++
+ //{{{ getScreenLineOfOffset() method
+ /**
+ * Returns the screen (wrapped) line containing the specified offset.
+
--- a/src/Tools/jEdit/src/plugin.scala Mon Sep 03 18:12:59 2012 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Mon Sep 03 22:51:33 2012 +0200
@@ -34,8 +34,11 @@
{
/* plugin instance */
- var plugin: Plugin = null
- var session: Session = null
+ @volatile var startup_failure: Option[Throwable] = None
+ @volatile var startup_notified = false
+
+ @volatile var plugin: Plugin = null
+ @volatile var session: Session = new Session(new JEdit_Thy_Load(Set.empty, Outer_Syntax.empty))
def thy_load(): JEdit_Thy_Load =
session.thy_load.asInstanceOf[JEdit_Thy_Load]
@@ -43,8 +46,8 @@
def get_recent_syntax(): Option[Outer_Syntax] =
{
val current_session = session
- if (current_session != null) Some(current_session.recent_syntax)
- else None
+ if (current_session.recent_syntax == Outer_Syntax.empty) None
+ else Some(current_session.recent_syntax)
}
@@ -316,11 +319,11 @@
modes ::: List(logic)
}
- def session_content(): Build.Session_Content =
+ def session_content(inlined_files: Boolean): Build.Session_Content =
{
val dirs = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
val name = Path.explode(session_args().last).base.implode // FIXME more robust
- Build.session_content(dirs, name).check_errors
+ Build.session_content(inlined_files, dirs, name).check_errors
}
@@ -373,7 +376,7 @@
val thy_info = new Thy_Info(Isabelle.thy_load)
// FIXME avoid I/O in Swing thread!?!
- val files = thy_info.dependencies(thys).deps.map(_._1.node).
+ val files = thy_info.dependencies(true, thys).deps.map(_._1.node).
filter(file => !loaded_buffer(file) && Isabelle.thy_load.check_file(view, file))
if (!files.isEmpty) {
@@ -432,60 +435,83 @@
override def handleMessage(message: EBMessage)
{
Swing_Thread.assert()
- message match {
- case msg: EditorStarted =>
- if (Isabelle.Boolean_Property("auto-start"))
- Isabelle.session.start(Isabelle.session_args())
- case msg: BufferUpdate
- if msg.getWhat == BufferUpdate.LOADED || msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
- if (Isabelle.session.is_ready) {
- val buffer = msg.getBuffer
- if (buffer != null && !buffer.isLoading) Isabelle.init_model(buffer)
- delay_load(true)
- }
+ if (Isabelle.startup_failure.isDefined && !Isabelle.startup_notified) {
+ message match {
+ case msg: EditorStarted =>
+ Library.error_dialog(null, "Isabelle plugin startup failure",
+ Library.scrollable_text(Exn.message(Isabelle.startup_failure.get)),
+ "Prover IDE inactive!")
+ Isabelle.startup_notified = true
+ case _ =>
+ }
+ }
+
+ if (Isabelle.startup_failure.isEmpty) {
+ message match {
+ case msg: EditorStarted =>
+ if (Isabelle.Boolean_Property("auto-start"))
+ Isabelle.session.start(Isabelle.session_args())
- case msg: EditPaneUpdate
- if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGING ||
- msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
- msg.getWhat == EditPaneUpdate.CREATED ||
- msg.getWhat == EditPaneUpdate.DESTROYED) =>
- val edit_pane = msg.getEditPane
- val buffer = edit_pane.getBuffer
- val text_area = edit_pane.getTextArea
+ case msg: BufferUpdate
+ if msg.getWhat == BufferUpdate.LOADED || msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
+ if (Isabelle.session.is_ready) {
+ val buffer = msg.getBuffer
+ if (buffer != null && !buffer.isLoading) Isabelle.init_model(buffer)
+ delay_load(true)
+ }
- if (buffer != null && text_area != null) {
- if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
- msg.getWhat == EditPaneUpdate.CREATED) {
- if (Isabelle.session.is_ready)
- Isabelle.init_view(buffer, text_area)
+ case msg: EditPaneUpdate
+ if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGING ||
+ msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
+ msg.getWhat == EditPaneUpdate.CREATED ||
+ msg.getWhat == EditPaneUpdate.DESTROYED) =>
+ val edit_pane = msg.getEditPane
+ val buffer = edit_pane.getBuffer
+ val text_area = edit_pane.getTextArea
+
+ if (buffer != null && text_area != null) {
+ if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
+ msg.getWhat == EditPaneUpdate.CREATED) {
+ if (Isabelle.session.is_ready)
+ Isabelle.init_view(buffer, text_area)
+ }
+ else Isabelle.exit_view(buffer, text_area)
}
- else Isabelle.exit_view(buffer, text_area)
- }
- case msg: PropertiesChanged =>
- Isabelle.setup_tooltips()
- Isabelle.session.global_settings.event(Session.Global_Settings)
+ case msg: PropertiesChanged =>
+ Isabelle.setup_tooltips()
+ Isabelle.session.global_settings.event(Session.Global_Settings)
- case _ =>
+ case _ =>
+ }
}
}
override def start()
- { // FIXME more robust error handling
- Isabelle.plugin = this
- Isabelle.setup_tooltips()
- Isabelle_System.init()
- Isabelle_System.install_fonts()
+ {
+ try {
+ Isabelle.plugin = this
+ Isabelle.setup_tooltips()
+ Isabelle_System.init()
+ Isabelle_System.install_fonts()
+
+ SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender)
+ if (ModeProvider.instance.isInstanceOf[ModeProvider])
+ ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)
- val content = Isabelle.session_content()
- val thy_load = new JEdit_Thy_Load(content.loaded_theories, content.syntax)
- Isabelle.session = new Session(thy_load)
+ val content = Isabelle.session_content(false)
+ val thy_load = new JEdit_Thy_Load(content.loaded_theories, content.syntax)
+ Isabelle.session = new Session(thy_load)
- SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender)
- if (ModeProvider.instance.isInstanceOf[ModeProvider])
- ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)
- Isabelle.session.phase_changed += session_manager
+ Isabelle.session.phase_changed += session_manager
+ Isabelle.startup_failure = None
+ }
+ catch {
+ case exn: Throwable =>
+ Isabelle.startup_failure = Some(exn)
+ Isabelle.startup_notified = false
+ }
}
override def stop()
--- a/src/Tools/jEdit/src/text_area_painter.scala Mon Sep 03 18:12:59 2012 +0200
+++ b/src/Tools/jEdit/src/text_area_painter.scala Mon Sep 03 22:51:33 2012 +0200
@@ -161,41 +161,6 @@
/* text */
- private def line_infos(physical_lines: Iterator[Int]): Map[Text.Offset, Chunk] =
- {
- val painter = text_area.getPainter
- val font = painter.getFont
- val font_context = painter.getFontRenderContext
-
- // see org.gjt.sp.jedit.textarea.TextArea.propertiesChanged
- // see org.gjt.sp.jedit.textarea.TextArea.setMaxLineLength
- val margin =
- if (buffer.getStringProperty("wrap") != "soft") 0.0f
- else {
- val max = buffer.getIntegerProperty("maxLineLen", 0)
- if (max > 0) font.getStringBounds(" " * max, font_context).getWidth.toInt
- else painter.getWidth - char_width() * 3
- }.toFloat
-
- val out = new ArrayList[Chunk]
- val handler = new DisplayTokenHandler
-
- var result = Map[Text.Offset, Chunk]()
- for (line <- physical_lines) {
- val line_start = buffer.getLineStartOffset(line)
-
- out.clear
- handler.init(painter.getStyles, font_context, painter, out, margin, line_start)
- buffer.markTokens(line, handler)
-
- for (i <- 0 until out.size) {
- val chunk = out.get(i)
- result += (line_start + chunk.offset -> chunk)
- }
- }
- result
- }
-
private def paint_chunk_list(snapshot: Document.Snapshot,
gfx: Graphics2D, line_start: Text.Offset, head: Chunk, x: Float, y: Float): Float =
{
@@ -287,21 +252,20 @@
val fm = text_area.getPainter.getFontMetrics
var y0 = y + fm.getHeight - (fm.getLeading + 1) - fm.getDescent
- val infos = line_infos(physical_lines.iterator.filter(i => i != -1))
for (i <- 0 until physical_lines.length) {
- if (physical_lines(i) != -1) {
- val x1 =
- infos.get(start(i)) match {
- case None => x0
- case Some(chunk) =>
- gfx.clipRect(x0, y + line_height * i, Integer.MAX_VALUE, line_height)
- val w = paint_chunk_list(snapshot, gfx, start(i), chunk, x0, y0).toInt
- x0 + w.toInt
- }
- gfx.clipRect(x1, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
- orig_text_painter.paintValidLine(gfx,
- first_line + i, physical_lines(i), start(i), end(i), y + line_height * i)
- gfx.setClip(clip)
+ val line = physical_lines(i)
+ if (line != -1) {
+ val screen_line = first_line + i
+ val chunks = text_area.getChunksOfScreenLine(screen_line)
+ if (chunks != null) {
+ val line_start = text_area.getBuffer.getLineStartOffset(line)
+ gfx.clipRect(x0, y + line_height * i, Integer.MAX_VALUE, line_height)
+ val w = paint_chunk_list(snapshot, gfx, line_start, chunks, x0, y0).toInt
+ gfx.clipRect(x0 + w.toInt, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
+ orig_text_painter.paintValidLine(gfx,
+ screen_line, line, start(i), end(i), y + line_height * i)
+ gfx.setClip(clip)
+ }
}
y0 += line_height
}