1/* Title: Tools/VSCode/src/grammar.scala 2 Author: Makarius 3 4Generate static TextMate grammar for VSCode editor. 5*/ 6 7package isabelle.vscode 8 9 10import isabelle._ 11 12 13object Grammar 14{ 15 /* generate grammar */ 16 17 lazy val default_logic = Isabelle_System.getenv("ISABELLE_LOGIC") 18 19 def default_output(logic: String = ""): String = 20 if (logic == "" || logic == default_logic) "isabelle-grammar.json" 21 else "isabelle-" + logic + "-grammar.json" 22 23 def generate(keywords: Keyword.Keywords): JSON.S = 24 { 25 val (minor_keywords, operators) = 26 keywords.minor.iterator.toList.partition(Symbol.is_ascii_identifier(_)) 27 28 def major_keywords(pred: String => Boolean): List[String] = 29 (for { 30 k <- keywords.major.iterator 31 kind <- keywords.kinds.get(k) 32 if pred(kind) 33 } yield k).toList 34 35 val keywords1 = 36 major_keywords(k => k != Keyword.THY_END && k != Keyword.PRF_ASM && k != Keyword.PRF_ASM_GOAL) 37 val keywords2 = minor_keywords ::: major_keywords(Set(Keyword.THY_END)) 38 val keywords3 = major_keywords(Set(Keyword.PRF_ASM, Keyword.PRF_ASM_GOAL)) 39 40 41 def grouped_names(as: List[String]): String = 42 JSON.Format("\\b(" + as.sorted.map(Library.escape_regex(_)).mkString("|") + ")\\b") 43 44 """{ 45 "name": "Isabelle", 46 "scopeName": "source.isabelle", 47 "fileTypes": ["thy"], 48 "uuid": """ + JSON.Format(UUID().toString) + """, 49 "repository": { 50 "comment": { 51 "patterns": [ 52 { 53 "name": "comment.block.isabelle", 54 "begin": "\\(\\*", 55 "patterns": [{ "include": "#comment" }], 56 "end": "\\*\\)" 57 } 58 ] 59 }, 60 "cartouche": { 61 "patterns": [ 62 { 63 "name": "string.quoted.other.multiline.isabelle", 64 "begin": "(?:\\\\<open>|���)", 65 "patterns": [{ "include": "#cartouche" }], 66 "end": "(?:\\\\<close>|���)" 67 } 68 ] 69 } 70 }, 71 "patterns": [ 72 { 73 "include": "#comment" 74 }, 75 { 76 "include": "#cartouche" 77 }, 78 { 79 "name": "keyword.control.isabelle", 80 "match": """ + grouped_names(keywords1) + """ 81 }, 82 { 83 "name": "keyword.other.unit.isabelle", 84 "match": """ + grouped_names(keywords2) + """ 85 }, 86 { 87 "name": "keyword.operator.isabelle", 88 "match": """ + grouped_names(operators) + """ 89 }, 90 { 91 "name": "entity.name.type.isabelle", 92 "match": """ + grouped_names(keywords3) + """ 93 }, 94 { 95 "name": "constant.numeric.isabelle", 96 "match": "\\b\\d*\\.?\\d+\\b" 97 }, 98 { 99 "name": "string.quoted.double.isabelle", 100 "begin": "\"", 101 "patterns": [ 102 { 103 "name": "constant.character.escape.isabelle", 104 "match": """ + JSON.Format("""\\[\"]|\\\d\d\d""") + """ 105 } 106 ], 107 "end": "\"" 108 }, 109 { 110 "name": "string.quoted.backtick.isabelle", 111 "begin": "`", 112 "patterns": [ 113 { 114 "name": "constant.character.escape.isabelle", 115 "match": """ + JSON.Format("""\\[\`]|\\\d\d\d""") + """ 116 } 117 ], 118 "end": "`" 119 }, 120 { 121 "name": "string.quoted.verbatim.isabelle", 122 "begin": """ + JSON.Format("""\{\*""") + """, 123 "patterns": [ 124 { "match": """ + JSON.Format("""[^*]+|\*(?!\})""") + """ } 125 ], 126 "end": """ + JSON.Format("""\*\}""") + """ 127 } 128 ] 129} 130""" 131 } 132 133 134 /* Isabelle tool wrapper */ 135 136 val isabelle_tool = Isabelle_Tool("vscode_grammar", 137 "generate static TextMate grammar for VSCode editor", args => 138 { 139 var dirs: List[Path] = Nil 140 var logic = default_logic 141 var output: Option[Path] = None 142 143 val getopts = Getopts(""" 144Usage: isabelle vscode_grammar [OPTIONS] 145 146 Options are: 147 -d DIR include session directory 148 -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(default_logic) + """) 149 -o FILE output file name (default """ + default_output() + """) 150 151 Generate static TextMate grammar for VSCode editor. 152""", 153 "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), 154 "l:" -> (arg => logic = arg), 155 "o:" -> (arg => output = Some(Path.explode(arg)))) 156 157 val more_args = getopts(args) 158 if (more_args.nonEmpty) getopts.usage() 159 160 val keywords = 161 Sessions.base_info(Options.init(), logic, dirs = dirs).check_base.overall_syntax.keywords 162 val output_path = output getOrElse Path.explode(default_output(logic)) 163 164 Output.writeln(output_path.implode) 165 File.write_backup(output_path, generate(keywords)) 166 }) 167} 168