diff -r f5da84211ac0 -r 417fcf9f5e71 src/Pure/Build/build_manager.scala --- a/src/Pure/Build/build_manager.scala Tue Jul 09 13:58:43 2024 +0200 +++ b/src/Pure/Build/build_manager.scala Tue Jul 09 14:13:59 2024 +0200 @@ -1071,6 +1071,7 @@ val HOME = Path.basic("home") val OVERVIEW = Path.basic("overview") val BUILD = Path.basic("build") + val DIFF = Path.basic("diff") } def paths(store: Store): Web_App.Paths = @@ -1121,6 +1122,7 @@ case Home(state: State) extends Model case Overview(kind: String, state: State) extends Model case Details(build: Build, state: State, public: Boolean = true) extends Model + case Diff(build: Build, state: State) extends Model } object View { @@ -1216,31 +1218,22 @@ submit_form("", List(hidden(ID, uuid.toString), api_button(paths.api_route(API.BUILD_CANCEL), "cancel build"))))) - def render_diff(diff: String): XML.Body = { - val Colored = "\u001b\\[([0-9;]+)m(.*)\u001b\\[0m".r - val colors = List("black", "red", "green", "yellow", "blue", "magenta", "cyan", "white") - - val lines = split_lines(diff).map { - case Colored(code, s) => - val codes = space_explode(';', code.stripSuffix(";1")).map(Value.Int.parse) - val fg = codes match { case 0 :: i :: Nil => colors.unapply(i - 30) case _ => None } + def non_local(components: List[Component]): List[Component] = + for (component <- components if !component.is_local) yield component - val sp = span(if (code.endsWith(";1")) List(bold(text(s))) else text(s)) - List(fg.map(color => sp + ("style" -> ("color:" + color))).getOrElse(sp)) - case line => text(Library.strip_ansi_color(line)) - } + def render_rev(components: List[Component], data: Report.Data): XML.Body = { + val relevant = non_local(components) + val hg_info = data.component_logs.map(_._1) ++ data.component_diffs.map(_._1) + val s = relevant.mkString(", ") - List(source(Library.separate(nl, lines).flatten)) + if (!relevant.map(_.name).exists(hg_info.toSet)) text(s) + else List(page_link(Page.DIFF, s, Markup.Name(build.name))) } - def render_rev(components: List[Component], diffs: Map[String, String]): XML.Body = - for (component <- components if !component.is_local) - yield par(text(component.toString) ++ diffs.get(component.name).flatMap(render_diff)) - build match { case task: Task => par(text("Task from " + Build_Log.print_date(task.submit_date) + ". ")) :: - render_rev(task.components, Map.empty) ::: + par(text(non_local(task.components).mkString(", "))) :: render_cancel(task.uuid) case job: Job => @@ -1250,8 +1243,8 @@ par( if (job.cancelled) text("Cancelling ...") else text("Running ...") ::: render_cancel(job.uuid)) :: - render_rev(job.components, report_data.component_diffs.toMap) ::: - par(text("Log") :+ source(report_data.build_log)) :: Nil + par(render_rev(job.components, report_data)) :: + par(List(source(report_data.build_log))) :: Nil case result: Result => val report_data = cache.lookup(store.report(result.kind, result.id)) @@ -1260,11 +1253,48 @@ if_proper(result.end_date, ", took " + (result.end_date.get - result.start_date).message_hms))) :: par(text("Status: " + result.status)) :: - render_rev(result.components, report_data.component_diffs.toMap) ::: - par(text("Log") :+ source(report_data.build_log)) :: Nil + par(render_rev(result.components, report_data)) :: + par(List(source(report_data.build_log))) :: Nil } } + def render_diff(build: Build, state: State): XML.Body = render_page("Diff: " + build.name) { + def colored(s: String): XML.Body = { + val Colored = "([^\u001b]*)\u001b\\[([0-9;]+)m(.*)\u001b\\[0m([^\u001b]*)".r + val colors = List("black", "red", "green", "yellow", "blue", "magenta", "cyan", "white") + + val lines = split_lines(s).map { + case Colored(pre, code, s, post) => + val codes = space_explode(';', code.stripSuffix(";1")).map(Value.Int.parse) + val fg = codes match { case 0 :: i :: Nil => colors.unapply(i - 30) case _ => None } + + val sp = span(if (code.endsWith(";1")) List(bold(text(s))) else text(s)) + val sp1 = fg.map(color => sp + ("style" -> ("color:" + color))).getOrElse(sp) + List(span(text(pre)), sp1, span(text(post))) + case line => text(Library.strip_ansi_color(line)) + } + + List(source(Library.separate(nl, lines).flatten)) + } + + def render_diff(data: Report.Data, components: List[Component]): XML.Body = + par(List(page_link(Page.BUILD, "back to build", Markup.Name(build.name)))) :: + (for (component <- components if !component.is_local) yield { + par( + text(component.name) ::: + data.component_logs.toMap.get(component.name).toList.flatMap(colored) ::: + data.component_diffs.toMap.get(component.name).toList.flatMap(colored)) + }) + + build match { + case job: Job => + render_diff(cache.lookup(store.report(job.kind, job.id)), job.components) + case result: Result => + render_diff(cache.lookup(store.report(result.kind, result.id)), result.components) + case _ => Nil + } + } + def render_cancelled: XML.Body = render_page("Build cancelled")(List(page_link(Page.HOME, "Home"))) @@ -1297,6 +1327,14 @@ case _ => None } + def get_diff(props: Properties.T): Option[Model.Diff] = + props match { + case Markup.Name(name) => + val state = _state + state.get(name).map(Model.Diff(_, state)) + case _ => None + } + def cancel_build(params: Params.Data): Option[Model] = for { uuid <- View.parse_uuid(params) @@ -1321,6 +1359,7 @@ case Model.Home(state) => View.render_home(state) case Model.Overview(kind, state) => View.render_overview(kind, state) case Model.Details(build, state, public) => View.render_details(build, state, public) + case Model.Diff(build, state) => View.render_diff(build, state) case Model.Cancelled => View.render_cancelled }) @@ -1329,6 +1368,7 @@ Get(Page.HOME, "home", _ => overview), Get(Page.OVERVIEW, "overview", get_overview), Get(Page.BUILD, "build", get_build), + Get(Page.DIFF, "diff", get_diff), Post(API.BUILD_CANCEL, "cancel build", cancel_build)) val logo = Bytes.read(Path.explode("$ISABELLE_HOME/lib/logo/isabelle_transparent-48.gif")) val head =