--- a/src/Pure/System/isabelle_tool.scala Sun Jan 01 23:08:39 2017 +0100
+++ b/src/Pure/System/isabelle_tool.scala Sun Jan 01 23:19:34 2017 +0100
@@ -114,6 +114,7 @@
Update_Header.isabelle_tool,
Update_Then.isabelle_tool,
Update_Theorems.isabelle_tool,
+ isabelle.vscode.Grammar.isabelle_tool,
isabelle.vscode.Server.isabelle_tool)
private def list_internal(): List[(String, String)] =
--- a/src/Pure/Tools/build.scala Sun Jan 01 23:08:39 2017 +0100
+++ b/src/Pure/Tools/build.scala Sun Jan 01 23:19:34 2017 +0100
@@ -235,8 +235,8 @@
session_dependencies(options, inlined_files, dirs, List(session))(session)
}
- def outer_syntax(options: Options, session: String): Outer_Syntax =
- session_content(options, false, Nil, session).syntax
+ def outer_syntax(options: Options, dirs: List[Path], session: String): Outer_Syntax =
+ session_content(options, false, dirs, session).syntax
/* jobs */
--- a/src/Pure/build-jars Sun Jan 01 23:08:39 2017 +0100
+++ b/src/Pure/build-jars Sun Jan 01 23:19:34 2017 +0100
@@ -160,6 +160,7 @@
../Tools/Graphview/tree_panel.scala
../Tools/VSCode/src/channel.scala
../Tools/VSCode/src/document_model.scala
+ ../Tools/VSCode/src/grammar.scala
../Tools/VSCode/src/protocol.scala
../Tools/VSCode/src/server.scala
../Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/extension/package.json Sun Jan 01 23:08:39 2017 +0100
+++ b/src/Tools/VSCode/extension/package.json Sun Jan 01 23:19:34 2017 +0100
@@ -29,6 +29,11 @@
"configuration": "./isabelle-language.json"
}
],
+ "grammars": [{
+ "language": "isabelle",
+ "scopeName": "source.isabelle",
+ "path": "./isabelle-grammar.json"
+ }],
"configuration": {
"title": "Isabelle",
"properties": {
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/src/grammar.scala Sun Jan 01 23:19:34 2017 +0100
@@ -0,0 +1,154 @@
+/* Title: Tools/VSCode/src/grammar.scala
+ Author: Makarius
+
+Generate static TextMate grammar for VSCode editor.
+*/
+
+package isabelle.vscode
+
+
+import isabelle._
+
+
+object Grammar
+{
+ /* generate grammar */
+
+ private lazy val default_logic = Isabelle_System.getenv("ISABELLE_LOGIC")
+
+ private def default_output(logic: String = ""): String =
+ if (logic == default_logic) "isabelle-grammar.json"
+ else "isabelle-" + logic + "-grammar.json"
+
+ def generate(
+ options: Options,
+ session_dirs: List[Path] = Nil,
+ session_name: String = default_logic,
+ output: Path = Path.explode(default_output()))
+ {
+ val keywords = Build.outer_syntax(options, session_dirs, session_name).keywords
+
+ 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 = major_keywords(Set(Keyword.THY_END))
+ val keywords3 = major_keywords(Set(Keyword.PRF_ASM, Keyword.PRF_ASM_GOAL))
+
+
+ def quote_name(a: String): String =
+ if (Symbol.is_ascii_identifier(a)) a else "\\Q" + a + "\\E"
+
+ def grouped_names(as: List[String]): String =
+ JSON.Format("\\b(" + as.sorted.map(quote_name(_)).mkString("|") + ")\\b")
+
+ File.write(output, """{
+ "name": "Isabelle",
+ "scopeName": "source.isabelle",
+ "fileTypes": ["thy"],
+ "uuid": "fb16e918-d05b-11e6-918e-2bb94aa2c605",
+ "repository": {
+ "comments": {
+ "patterns": [
+ {
+ "name": "comment.block.isabelle",
+ "begin": "\\(\\*",
+ "beginCaptures": {
+ "0": { "name": "punctuation.definition.comment.begin.isabelle" }
+ },
+ "patterns": [{ "include": "#comments" }],
+ "end": "\\*\\)",
+ "endCaptures": {
+ "0": { "name": "punctuation.definition.comment.end.isabelle" }
+ }
+ }
+ ]
+ }
+ },
+ "patterns": [
+ {
+ "include": "#comments"
+ },
+ {
+ "name": "keyword.control.isabelle",
+ "match": """ + grouped_names(keywords1) + """
+ },
+ {
+ "name": "keyword.other.isabelle",
+ "match": """ + grouped_names(keywords2) + """
+ },
+ {
+ "name": "keyword.operator.isabelle",
+ "match": """ + grouped_names(operators) + """
+ },
+ {
+ "name": "constant.language.isabelle",
+ "match": """ + grouped_names(keywords3) + """
+ },
+ {
+ "match": "\\b\\d*\\.?\\d+\\b",
+ "name": "constant.numeric.isabelle"
+ },
+ {
+ "name": "string.quoted.double.isabelle",
+ "begin": "\"",
+ "beginCaptures": {
+ "0": { "name": "punctuation.definition.string.begin.isabelle" }
+ },
+ "patterns": [
+ {
+ "match": "\\\\.",
+ "name": "constant.character.escape.isabelle"
+ }
+ ],
+ "end": "\"",
+ "endCaptures": {
+ "0": { "name": "punctuation.definition.string.end.isabelle" }
+ }
+ }
+ ]
+}
+""")
+ }
+
+
+ /* Isabelle tool wrapper */
+
+ val isabelle_tool = Isabelle_Tool("vscode_grammar",
+ "generate static TextMate grammar for VSCode editor", 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 output_path = output getOrElse Path.explode(default_output(logic))
+ Output.writeln(output_path.implode)
+
+ generate(Options.init(), dirs, logic, output_path)
+ })
+}