--- a/etc/build.props Mon Mar 21 10:32:24 2022 +0100
+++ b/etc/build.props Mon Mar 21 10:56:29 2022 +0100
@@ -219,7 +219,6 @@
src/Tools/VSCode/src/lsp.scala \
src/Tools/VSCode/src/preview_panel.scala \
src/Tools/VSCode/src/state_panel.scala \
- src/Tools/VSCode/src/textmate_grammar.scala \
src/Tools/VSCode/src/vscode_model.scala \
src/Tools/VSCode/src/vscode_rendering.scala \
src/Tools/VSCode/src/vscode_resources.scala \
--- a/src/Pure/System/isabelle_tool.scala Mon Mar 21 10:32:24 2022 +0100
+++ b/src/Pure/System/isabelle_tool.scala Mon Mar 21 10:56:29 2022 +0100
@@ -210,7 +210,6 @@
Update_Then.isabelle_tool,
Update_Theorems.isabelle_tool,
isabelle.mirabelle.Mirabelle.isabelle_tool,
- isabelle.vscode.TextMate_Grammar.isabelle_tool,
isabelle.vscode.Language_Server.isabelle_tool)
class Admin_Tools extends Isabelle_Scala_Tools(
--- a/src/Tools/VSCode/src/build_vscode_extension.scala Mon Mar 21 10:32:24 2022 +0100
+++ b/src/Tools/VSCode/src/build_vscode_extension.scala Mon Mar 21 10:56:29 2022 +0100
@@ -12,19 +12,129 @@
object Build_VSCode
{
- val extension_dir = Path.explode("$ISABELLE_VSCODE_HOME/extension")
+ val extension_dir: Path = Path.explode("$ISABELLE_VSCODE_HOME/extension")
- /* grammar */
+ /* build grammar */
+
+ def default_logic: String = Isabelle_System.getenv("ISABELLE_LOGIC")
- def build_grammar(options: Options, progress: Progress = new Progress): Unit =
+ def build_grammar(options: Options,
+ logic: String = default_logic,
+ dirs: List[Path] = Nil,
+ progress: Progress = new Progress): Unit =
{
- val logic = TextMate_Grammar.default_logic
- val keywords = Sessions.base_info(options, logic).check.base.overall_syntax.keywords
+ val keywords =
+ Sessions.base_info(options, logic, dirs = dirs).check.base.overall_syntax.keywords
+
+ val output_path = extension_dir + Path.explode("isabelle-grammar.json")
+ progress.echo(output_path.expand.implode)
+
+ 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")
- val output_path = extension_dir + Path.explode(TextMate_Grammar.default_output(logic))
- progress.echo(output_path.expand.implode)
- File.write_backup(output_path, TextMate_Grammar.generate(keywords))
+ File.write_backup(output_path, """{
+ "name": "Isabelle",
+ "scopeName": "source.isabelle",
+ "fileTypes": ["thy"],
+ "uuid": """ + JSON.Format(UUID.random().toString) + """,
+ "repository": {
+ "comment": {
+ "patterns": [
+ {
+ "name": "comment.block.isabelle",
+ "begin": "\\(\\*",
+ "patterns": [{ "include": "#comment" }],
+ "end": "\\*\\)"
+ }
+ ]
+ },
+ "cartouche": {
+ "patterns": [
+ {
+ "name": "string.quoted.other.multiline.isabelle",
+ "begin": "(?:\\\\<open>|‹)",
+ "patterns": [{ "include": "#cartouche" }],
+ "end": "(?:\\\\<close>|›)"
+ }
+ ]
+ }
+ },
+ "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("""\*\}""") + """
+ }
+ ]
+}
+""")
}
@@ -64,6 +174,8 @@
Isabelle_Tool("build_vscode_extension", "build Isabelle/VSCode extension module",
Scala_Project.here, args =>
{
+ var dirs: List[Path] = Nil
+ var logic = default_logic
var install = false
var uninstall = false
@@ -73,10 +185,13 @@
Options are:
-I install resulting extension
-U uninstall extension (no build)
+ -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(default_logic) + """)
Build Isabelle/VSCode extension module in directory
""" + extension_dir.expand + """
""",
+ "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
+ "l:" -> (arg => logic = arg),
"I" -> (_ => install = true),
"U" -> (_ => uninstall = true))
@@ -90,7 +205,7 @@
uninstall_extension(progress = progress)
}
else {
- build_grammar(options, progress = progress)
+ build_grammar(options, logic = logic, dirs = dirs, progress = progress)
val path = build_extension(progress = progress)
if (install) install_extension(path, progress = progress)
}
--- a/src/Tools/VSCode/src/textmate_grammar.scala Mon Mar 21 10:32:24 2022 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,167 +0,0 @@
-/* Title: Tools/VSCode/src/textmate_grammar.scala
- Author: Makarius
-
-Generate static TextMate grammar for VSCode editor.
-*/
-
-package isabelle.vscode
-
-
-import isabelle._
-
-
-object TextMate_Grammar
-{
- /* generate grammar */
-
- lazy val default_logic = Isabelle_System.getenv("ISABELLE_LOGIC")
-
- def default_output(logic: String = ""): String =
- if (logic == "" || logic == default_logic) "isabelle-grammar.json"
- else "isabelle-" + logic + "-grammar.json"
-
- def generate(keywords: Keyword.Keywords): JSON.S =
- {
- 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")
-
- """{
- "name": "Isabelle",
- "scopeName": "source.isabelle",
- "fileTypes": ["thy"],
- "uuid": """ + JSON.Format(UUID.random().toString) + """,
- "repository": {
- "comment": {
- "patterns": [
- {
- "name": "comment.block.isabelle",
- "begin": "\\(\\*",
- "patterns": [{ "include": "#comment" }],
- "end": "\\*\\)"
- }
- ]
- },
- "cartouche": {
- "patterns": [
- {
- "name": "string.quoted.other.multiline.isabelle",
- "begin": "(?:\\\\<open>|‹)",
- "patterns": [{ "include": "#cartouche" }],
- "end": "(?:\\\\<close>|›)"
- }
- ]
- }
- },
- "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("""\*\}""") + """
- }
- ]
-}
-"""
- }
-
-
- /* Isabelle tool wrapper */
-
- val isabelle_tool = Isabelle_Tool("vscode_grammar",
- "generate static TextMate grammar for VSCode editor", Scala_Project.here, args =>
- {
- var dirs: List[Path] = Nil
- var logic = default_logic
- var output: Option[Path] = None
-
- val getopts = Getopts("""
-Usage: isabelle vscode_grammar [OPTIONS]
-
- Options are:
- -d DIR include session directory
- -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(default_logic) + """)
- -o FILE output file name (default """ + default_output() + """)
-
- Generate static TextMate grammar for VSCode editor.
-""",
- "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
- "l:" -> (arg => logic = arg),
- "o:" -> (arg => output = Some(Path.explode(arg))))
-
- val more_args = getopts(args)
- if (more_args.nonEmpty) getopts.usage()
-
- val keywords =
- Sessions.base_info(Options.init(), logic, dirs = dirs).check.base.overall_syntax.keywords
- val output_path = output getOrElse Path.explode(default_output(logic))
-
- Output.writeln(output_path.implode)
- File.write_backup(output_path, generate(keywords))
- })
-}