# HG changeset patch # User wenzelm # Date 1346705493 -7200 # Node ID aa09d99bf414d7e5790ad3286e4f377d6560a85f # Parent a426099dc343c8e1acaf65dd1175a63d6ce06d7f# Parent 21c8d2070be9a8afed67e5022fd01b9b7ecf8d4d merged diff -r a426099dc343 -r aa09d99bf414 Admin/component_repository/components.sha1 --- 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 diff -r a426099dc343 -r aa09d99bf414 Admin/components/main --- 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 diff -r a426099dc343 -r aa09d99bf414 src/Pure/System/build.scala --- 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 = diff -r a426099dc343 -r aa09d99bf414 src/Pure/Thy/thy_info.scala --- 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) } diff -r a426099dc343 -r aa09d99bf414 src/Tools/jEdit/patches/jedit-4.5.2/chunks --- /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. + diff -r a426099dc343 -r aa09d99bf414 src/Tools/jEdit/src/plugin.scala --- 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() diff -r a426099dc343 -r aa09d99bf414 src/Tools/jEdit/src/text_area_painter.scala --- 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 }