Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/Isabelle/Tools/VSCode/src/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 3 kB

Quelle pretty_text_panel.scala Sprache: Scala

/*  Title:      Tools/VSCode/src/pretty_text_panel.scala
    Author:     Thomas Lindae, TU Muenchen

Pretty-printed text or HTML with decorations.
*/

package isabelle.vscode

import isabelle._

object Pretty_Text_Panel {
  def apply(
    session: VSCode_Session,
    channel: Channel,
    output: (String, Option[LSP.Decoration]) => JSON.T
  ): Pretty_Text_Panel = new Pretty_Text_Panel(session, channel, output)
}

class Pretty_Text_Panel private(
  session: VSCode_Session,
  channel: Channel,
  output_json: (String, Option[LSP.Decoration]) => JSON.T
) {
  def resources: VSCode_Resources = session.resources

  private var current_output: List[XML.Elem] = Nil
  private var current_formatted: XML.Body = Nil
  private var margin: Double = resources.message_margin

  private val delay_margin = Delay.last(resources.output_delay, channel.Error_Logger) {
    refresh(current_output)
  }

  def update_margin(new_margin: Double): Unit = {
    margin = new_margin
    delay_margin.invoke()
  }

  def refresh(output: List[XML.Elem]): Unit = {
    val formatted =
      Pretty.formatted(Pretty.separate(output), margin = margin, metric = Symbol.Metric)

    if (formatted != current_formatted) {
      val message = {
        if (resources.html_output) {
          val node_context =
            new Browser_Info.Node_Context {
              override def make_ref(props: Properties.T, body: XML.Body): Option[XML.Elem] =
                for {
                  thy_file <- Position.Def_File.unapply(props)
                  def_line <- Position.Def_Line.unapply(props)
                  platform_path <- session.store.source_file(thy_file)
                  uri = File.uri(Path.explode(File.standard_path(platform_path)).absolute_file)
                } yield HTML.link(uri.toString + "#" + def_line, body)
            }
          val elements = Browser_Info.extra_elements.copy(entity = Markup.Elements.full)
          val html = node_context.make_html(elements, formatted)
          output_json(HTML.source(html).toString, None)
        }
        else {
          val converted = resources.output_text_xml(formatted)
          val converted_tree = Markup_Tree.from_XML(converted)
          val converted_text = XML.content(converted)

          val document = Line.Document(converted_text)
          val markups =
            converted_tree.cumulate[Option[Markup]](
              Text.Range.full, None, Rendering.text_color_elements,
              { case (_, m) => Some(Some(m.info.markup)) })
          val entries =
            (for {
              case Text.Info(range, Some(markup)) <- markups
              color <- Rendering.get_text_color(markup)
            } yield color -> document.range(range))
              .groupMap(_._1)(p => LSP.Decoration_Range(p._2))
              .iterator.map({ case (c, rs) => LSP.Decoration_Entry.text_color(c, rs) })
              .toList

          output_json(converted_text, Some(LSP.Decoration(entries)))
        }
      }
      channel.write(message)
      current_output = output
      current_formatted = formatted
    }
  }
}

quality91%

¤ Dauer der Verarbeitung: 0.24 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.