# HG changeset patch # User wenzelm # Date 1535826050 -7200 # Node ID f5c76072db557d66ed6d5af807dc82b03679dfa4 # Parent 53a75627aab737c26a1ea974064f92658ef1ca89 more explicit status for "canceled" command within theory node; diff -r 53a75627aab7 -r f5c76072db55 src/Doc/System/Server.thy --- a/src/Doc/System/Server.thy Sat Sep 01 18:39:36 2018 +0200 +++ b/src/Doc/System/Server.thy Sat Sep 01 20:20:50 2018 +0200 @@ -516,14 +516,16 @@ session-qualified theory name (e.g.\ \<^verbatim>\HOL-ex.Seq\). \<^item> \<^bold>\type\ \node_status = {ok: bool, total: int, unprocessed: int, running: - int, warned: int, failed: int, finished: int, initialized: bool, - consolidated: bool}\ represents a formal theory node status of the PIDE - document model. Fields \total\, \unprocessed\, \running\, \warned\, + int, warned: int, failed: int, finished: int, canceled: bool, initialized: + bool, consolidated: bool}\ represents a formal theory node status of the + PIDE document model. Fields \total\, \unprocessed\, \running\, \warned\, \failed\, \finished\ account for individual commands within a theory node; - \ok\ is an abstraction for \failed = 0\. The \initialized\ flag indicates - that the initial \<^theory_text>\theory\ command has been processed. The \consolidated\ - flag indicates whether the outermost theory command structure has finished - (or failed) and the final \<^theory_text>\end\ command has been checked. + \ok\ is an abstraction for \failed = 0\. The \canceled\ flag tells if some + command in the theory has been spontaneously canceled (by an Interrupt + exception that could also indicate resource problems). The \initialized\ + flag indicates that the initial \<^theory_text>\theory\ command has been processed. The + \consolidated\ flag indicates whether the outermost theory command structure + has finished (or failed) and the final \<^theory_text>\end\ command has been checked. \ diff -r 53a75627aab7 -r f5c76072db55 src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML Sat Sep 01 18:39:36 2018 +0200 +++ b/src/Pure/PIDE/command.ML Sat Sep 01 20:20:50 2018 +0200 @@ -260,7 +260,7 @@ let val _ = status tr Markup.failed; val _ = status tr Markup.finished; - val _ = if null errs then (report tr (Markup.bad ()); Exn.interrupt ()) else (); + val _ = if null errs then (status tr Markup.canceled; Exn.interrupt ()) else (); in {failed = true, command = tr, state = st} end | SOME st' => let diff -r 53a75627aab7 -r f5c76072db55 src/Pure/PIDE/document_status.scala --- a/src/Pure/PIDE/document_status.scala Sat Sep 01 18:39:36 2018 +0200 +++ b/src/Pure/PIDE/document_status.scala Sat Sep 01 20:20:50 2018 +0200 @@ -15,7 +15,7 @@ { val proper_elements: Markup.Elements = Markup.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING, - Markup.FINISHED, Markup.FAILED) + Markup.FINISHED, Markup.FAILED, Markup.CANCELED) val liberal_elements: Markup.Elements = proper_elements + Markup.WARNING + Markup.LEGACY + Markup.ERROR @@ -26,6 +26,7 @@ var accepted = false var warned = false var failed = false + var canceled = false var forks = 0 var runs = 0 for (markup <- markup_iterator) { @@ -37,10 +38,11 @@ case Markup.FINISHED => runs -= 1 case Markup.WARNING | Markup.LEGACY => warned = true case Markup.FAILED | Markup.ERROR => failed = true + case Markup.CANCELED => canceled = true case _ => } } - Command_Status(touched, accepted, warned, failed, forks, runs) + Command_Status(touched, accepted, warned, failed, canceled, forks, runs) } val empty = make(Iterator.empty) @@ -58,6 +60,7 @@ private val accepted: Boolean, private val warned: Boolean, private val failed: Boolean, + private val canceled: Boolean, forks: Int, runs: Int) { @@ -67,6 +70,7 @@ accepted || that.accepted, warned || that.warned, failed || that.failed, + canceled || that.canceled, forks + that.forks, runs + that.runs) @@ -75,6 +79,7 @@ def is_warned: Boolean = warned def is_failed: Boolean = failed def is_finished: Boolean = !failed && touched && forks == 0 && runs == 0 + def is_canceled: Boolean = canceled } @@ -94,6 +99,7 @@ var warned = 0 var failed = 0 var finished = 0 + var canceled = false for (command <- node.commands.iterator) { val states = state.command_states(version, command) val status = Command_Status.merge(states.iterator.map(_.document_status)) @@ -103,17 +109,20 @@ else if (status.is_warned) warned += 1 else if (status.is_finished) finished += 1 else unprocessed += 1 + + if (status.is_canceled) canceled = true } val initialized = state.node_initialized(version, name) val consolidated = state.node_consolidated(version, name) - Node_Status(unprocessed, running, warned, failed, finished, initialized, consolidated) + Node_Status( + unprocessed, running, warned, failed, finished, canceled, initialized, consolidated) } } sealed case class Node_Status( unprocessed: Int, running: Int, warned: Int, failed: Int, finished: Int, - initialized: Boolean, consolidated: Boolean) + canceled: Boolean, initialized: Boolean, consolidated: Boolean) { def ok: Boolean = failed == 0 def total: Int = unprocessed + running + warned + failed + finished @@ -121,7 +130,7 @@ def json: JSON.Object.T = JSON.Object("ok" -> ok, "total" -> total, "unprocessed" -> unprocessed, "running" -> running, "warned" -> warned, "failed" -> failed, "finished" -> finished, - "initialized" -> initialized, "consolidated" -> consolidated) + "canceled" -> canceled, "initialized" -> initialized, "consolidated" -> consolidated) } diff -r 53a75627aab7 -r f5c76072db55 src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Sat Sep 01 18:39:36 2018 +0200 +++ b/src/Pure/PIDE/markup.ML Sat Sep 01 20:20:50 2018 +0200 @@ -165,6 +165,7 @@ val runningN: string val running: T val finishedN: string val finished: T val failedN: string val failed: T + val canceledN: string val canceled: T val initializedN: string val initialized: T val consolidatedN: string val consolidated: T val exec_idN: string @@ -577,7 +578,7 @@ val (runningN, running) = markup_elem "running"; val (finishedN, finished) = markup_elem "finished"; val (failedN, failed) = markup_elem "failed"; - +val (canceledN, canceled) = markup_elem "canceled"; val (initializedN, initialized) = markup_elem "initialized"; val (consolidatedN, consolidated) = markup_elem "consolidated"; diff -r 53a75627aab7 -r f5c76072db55 src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Sat Sep 01 18:39:36 2018 +0200 +++ b/src/Pure/PIDE/markup.scala Sat Sep 01 20:20:50 2018 +0200 @@ -424,7 +424,7 @@ val RUNNING = "running" val FINISHED = "finished" val FAILED = "failed" - + val CANCELED = "canceled" val INITIALIZED = "initialized" val CONSOLIDATED = "consolidated" diff -r 53a75627aab7 -r f5c76072db55 src/Pure/PIDE/rendering.scala --- a/src/Pure/PIDE/rendering.scala Sat Sep 01 18:39:36 2018 +0200 +++ b/src/Pure/PIDE/rendering.scala Sat Sep 01 20:20:50 2018 +0200 @@ -19,7 +19,7 @@ object Color extends Enumeration { // background - val unprocessed1, running1, bad, intensify, entity, active, active_result, + val unprocessed1, running1, canceled, bad, intensify, entity, active, active_result, markdown_bullet1, markdown_bullet2, markdown_bullet3, markdown_bullet4 = Value val background_colors = values @@ -432,6 +432,7 @@ val status = Document_Status.Command_Status.make(markups.iterator) if (status.is_unprocessed) Some(Rendering.Color.unprocessed1) else if (status.is_running) Some(Rendering.Color.running1) + else if (status.is_canceled) Some(Rendering.Color.canceled) else opt_color case (_, opt_color) => opt_color }) diff -r 53a75627aab7 -r f5c76072db55 src/Tools/VSCode/extension/package.json --- a/src/Tools/VSCode/extension/package.json Sat Sep 01 18:39:36 2018 +0200 +++ b/src/Tools/VSCode/extension/package.json Sat Sep 01 20:20:50 2018 +0200 @@ -250,6 +250,14 @@ "type": "string", "default": "rgba(255, 160, 160, 0.40)" }, + "isabelle.canceled_light_color": { + "type": "string", + "default": "rgba(255, 106, 106, 0.40)" + }, + "isabelle.canceled_dark_color": { + "type": "string", + "default": "rgba(255, 106, 106, 0.40)" + }, "isabelle.bad_light_color": { "type": "string", "default": "rgba(255, 106, 106, 0.40)" diff -r 53a75627aab7 -r f5c76072db55 src/Tools/VSCode/extension/src/decorations.ts --- a/src/Tools/VSCode/extension/src/decorations.ts Sat Sep 01 18:39:36 2018 +0200 +++ b/src/Tools/VSCode/extension/src/decorations.ts Sat Sep 01 20:20:50 2018 +0200 @@ -13,6 +13,7 @@ const background_colors = [ "unprocessed1", "running1", + "canceled", "bad", "intensify", "quoted", diff -r 53a75627aab7 -r f5c76072db55 src/Tools/jEdit/etc/options --- a/src/Tools/jEdit/etc/options Sat Sep 01 18:39:36 2018 +0200 +++ b/src/Tools/jEdit/etc/options Sat Sep 01 20:20:50 2018 +0200 @@ -95,6 +95,7 @@ option error_message_color : string = "FFC1C1FF" option spell_checker_color : string = "0000FFFF" option bad_color : string = "FF6A6A64" +option canceled_color : string = "FF6A6A64" option intensify_color : string = "FFCC6664" option entity_color : string = "CCD9FF80" option entity_ref_color : string = "800080FF"