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 9 kB

Quelle component_vscode_extension.scala Sprache: Scala

/*  Title:      Tools/VSCode/src/component_vscode_extension.scala
    Author:     Makarius

Build the Isabelle/VSCode extension as component.
*/

package isabelle.vscode

import isabelle._

object Component_VSCode {
  /* build grammar */

  def build_grammar(options: Options, build_dir: Path,
    logic: String = Isabelle_System.default_logic(),
    dirs: List[Path] = Nil,
    progress: Progress = new Progress
  ): Unit = {
    val keywords =
      Sessions.background(options, logic, dirs = dirs).check_errors.base.overall_syntax.keywords

    val output_path = build_dir + Path.explode("isabelle-grammar.json")
    progress.echo(File.standard_path(output_path))

    val (minor_keywords, operators) =
      keywords.minor.iterator.toList.partition(Symbol.is_ascii_identifier)

    def major_keywords(pred: String => Boolean): List[String] =
      (for {
        k <- keywords.major.iterator
        kind <- keywords.kinds.get(k)
        if pred(kind)
      } yield k).toList

    val keywords1 =
      major_keywords(k => k != Keyword.THY_END && k != Keyword.PRF_ASM && k != Keyword.PRF_ASM_GOAL)
    val keywords2 = minor_keywords ::: major_keywords(Set(Keyword.THY_END))
    val keywords3 = major_keywords(Set(Keyword.PRF_ASM, Keyword.PRF_ASM_GOAL))

    def grouped_names(as: List[String]): String =
      JSON.Format("\\b(" + as.sorted.map(Library.escape_regex).mkString("|") + ")\\b")

    File.write_backup(output_path, """{
  "name": "Isabelle",
  "scopeName": "source.isabelle",
  "fileTypes": ["thy"],
  "uuid": """ + JSON.Format(UUID.random_string()) + """,
  "repository": {
    "comment": {
      "patterns": [
        {
          "name": "comment.block.isabelle",
          "begin": "\$\\*",
          "patterns": [{ "include": "#comment" }],
          "end": "\\*\$"
        }
      ]
    },
    "cartouche": {
      "patterns": [
        {
          "name": "string.quoted.other.multiline.isabelle",
          "begin": "(?:\\\\|‹)",
          "patterns": [{ "include": "#cartouche" }],
          "end": "(?:\\\\|›)"
        }
      ]
    }
  },
  "patterns": [
    {
      "include": "#comment"
    },
    {
      "include": "#cartouche"
    },
    {
      "name": "keyword.control.isabelle",
      "match": """ + grouped_names(keywords1) + """
    },
    {
      "name": "keyword.other.unit.isabelle",
      "match": """ + grouped_names(keywords2) + """
    },
    {
      "name": "keyword.operator.isabelle",
      "match": """ + grouped_names(operators) + """
    },
    {
      "name": "entity.name.type.isabelle",
      "match": """ + grouped_names(keywords3) + """
    },
    {
      "name": "constant.numeric.isabelle",
      "match": "\\b\\d*\\.?\\d+\\b"
    },
    {
      "name": "string.quoted.double.isabelle",
      "begin": "\"",
      "patterns": [
        {
          "name": "constant.character.escape.isabelle",
          "match": """ + JSON.Format("""\\[\"]|\\\d\d\d""") + """
        }
      ],
      "end": "\""
    },
    {
      "name": "string.quoted.backtick.isabelle",
      "begin": "`",
      "patterns": [
        {
          "name": "constant.character.escape.isabelle",
          "match": """ + JSON.Format("""\\[\`]|\\\d\d\d""") + """
        }
      ],
      "end": "`"
    },
    {
      "name": "string.quoted.verbatim.isabelle",
      "begin": """ + JSON.Format("""\{\*""") + """,
      "patterns": [
        { "match": """ + JSON.Format("""[^*]+|\*(?!\})""") + """ }
      ],
      "end": """ + JSON.Format("""\*\}""") + """
    }
  ]
}
""")
  }


  private def options_json(options: Options): String = {
    val relevant_options =
      Set(
        "editor_output_state",
        "auto_time_start",
        "auto_time_limit",
        "auto_nitpick",
        "auto_sledgehammer",
        "auto_methods",
        "auto_quickcheck",
        "auto_solve_direct",
        "sledgehammer_provers",
        "sledgehammer_timeout")

    (for {
      opt <- options.iterator
      if opt.for_vscode || opt.for_content || relevant_options.contains(opt.name)
    } yield {
      val (enum_values, enum_descriptions) = opt.typ match {
        case Options.Bool => (
          Some(List("", "true", "false")),
          Some(List("Use System Preference.", "Enable.", "Disable.")))
        case _ => (None, None)
      }

      val default = opt.name match {
        case "vscode_unicode_symbols_output" => "true"
        case "vscode_unicode_symbols_edits" => "true"
        case "vscode_pide_extensions" => "true"
        case "vscode_html_output" => "true"
        case _ => ""
      }

      quote("isabelle.options." + opt.name) + ": " +
        JSON.Format(
          JSON.Object(
            "type" -> "string",
            "default" -> default,
            "description" -> opt.description) ++
          JSON.optional("enum" -> enum_values) ++
          JSON.optional("enumDescriptions" -> enum_descriptions)) + ","
    }).mkString
  }

  /* build extension */

  def build_extension(options: Options,
    target_dir: Path = Path.current,
    logic: String = Isabelle_System.default_logic(),
    dirs: List[Path] = Nil,
    progress: Progress = new Progress
  ): Unit = {
    /* component */

    val component_name = "vscode_extension-" + Date.Format.alt_date(Date.now())
    val component_dir =
      Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress)

    /* build */

    val vsix_name =
      Isabelle_System.with_tmp_dir("build") { build_dir =>
        val node_dir =
          Nodejs.setup(build_dir,
            platform_context = Isabelle_Platform.Context(progress = progress),
            packages = List("yarn", "vsce"))

        val manifest_text = File.read(VSCode_Main.extension_dir + VSCode_Main.MANIFEST)
        val manifest_entries = split_lines(manifest_text).filter(_.nonEmpty)
        for (name <- manifest_entries) {
          val path = Path.explode(name)
          Isabelle_System.copy_file(VSCode_Main.extension_dir + path,
            Isabelle_System.make_directory(build_dir + path.dir))
        }

        val fonts_dir = Isabelle_System.make_directory(build_dir + Path.basic("fonts"))
        for (entry <- Isabelle_Fonts.fonts()) { Isabelle_System.copy_file(entry.path, fonts_dir) }
        val manifest_text2 =
          manifest_text + cat_lines(Isabelle_Fonts.fonts().map(e => "fonts/" + e.path.file_name))
        val manifest_entries2 = split_lines(manifest_text2).filter(_.nonEmpty)

        val manifest_shasum: SHA1.Shasum = {
          val a = SHA1.shasum_meta_info(SHA1.digest(manifest_text2))
          val bs =
            for (name <- manifest_entries2)
              yield SHA1.shasum(SHA1.digest(build_dir + Path.explode(name)), name)
          SHA1.flat_shasum(a :: bs)
        }
        File.write(build_dir + VSCode_Main.MANIFEST.shasum, manifest_shasum.toString)

        /* options */

        val opt_json = options_json(options)
        val package_path = build_dir + Path.basic("package.json")
        val package_body = File.read(package_path).replace("\"ISABELLE_OPTIONS\": {},", opt_json)
        File.write(package_path, package_body)

        build_grammar(options, build_dir, logic = logic, dirs = dirs, progress = progress)

        val result =
          progress.bash(
            Library.make_lines(
              "set -e",
              node_dir.path_setup,
              "yarn",
              "vsce package"),
            cwd = build_dir, echo = true).check
        val Pattern = """.*Packaged:.*(isabelle-.*\.vsix).*""".r
        val vsix_name =
          result.out_lines.collectFirst({ case Pattern(name) => name })
            .getOrElse(error("Failed to guess resulting .vsix file name"))

        Isabelle_System.copy_file(build_dir + Path.basic(vsix_name), component_dir.path)
        vsix_name
      }

    /* settings */

    component_dir.write_settings("""
ISABELLE_VSCODE_VSIX="$COMPONENT/""" + vsix_name + "\"\n")

    /* README */

    File.write(component_dir.README,
      """This the Isabelle/VSCode extension as VSIX package

It has been produced from the sources in $ISABELLE_HOME/src/Tools/extension/.

        Makarius
        """ + Date.Format.date(Date.now()) + "\n")
  }

  /* Isabelle tool wrapper */

  val isabelle_tool =
    Isabelle_Tool("component_vscode_extension", "build Isabelle/VSCode extension module",
      Scala_Project.here,
      { args =>
        var target_dir = Path.current
        var dirs: List[Path] = Nil
        var logic = Isabelle_System.default_logic()

        val getopts = Getopts("""
Usage: isabelle component_vscode_extension

  Options are:
    -D DIR       target directory (default ".")
    -d DIR       include session directory
    -l NAME      logic session name (default ISABELLE_LOGIC=""" +
          quote(Isabelle_System.default_logic()) + """)

Build the Isabelle/VSCode extension as component, for inclusion into the
local VSCodium configuration.
""",
          "D:" -> (arg => target_dir = Path.explode(arg)),
          "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
          "l:" -> (arg => logic = arg))

        val more_args = getopts(args)
        if (more_args.nonEmpty) getopts.usage()

        val options = Options.init()
        val progress = new Console_Progress()

        build_extension(options, target_dir = target_dir, logic = logic, dirs = dirs,
          progress = progress)
      })
}

quality84%

¤ Dauer der Verarbeitung: 0.12 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.