src/Tools/VSCode/src/grammar.scala
changeset 64738 bcdecd466cb2
child 64739 3224021893c0
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/VSCode/src/grammar.scala	Sun Jan 01 23:19:34 2017 +0100
     1.3 @@ -0,0 +1,154 @@
     1.4 +/*  Title:      Tools/VSCode/src/grammar.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Generate static TextMate grammar for VSCode editor.
     1.8 +*/
     1.9 +
    1.10 +package isabelle.vscode
    1.11 +
    1.12 +
    1.13 +import isabelle._
    1.14 +
    1.15 +
    1.16 +object Grammar
    1.17 +{
    1.18 +  /* generate grammar */
    1.19 +
    1.20 +  private lazy val default_logic = Isabelle_System.getenv("ISABELLE_LOGIC")
    1.21 +
    1.22 +  private def default_output(logic: String = ""): String =
    1.23 +    if (logic == default_logic) "isabelle-grammar.json"
    1.24 +    else "isabelle-" + logic + "-grammar.json"
    1.25 +
    1.26 +  def generate(
    1.27 +    options: Options,
    1.28 +    session_dirs: List[Path] = Nil,
    1.29 +    session_name: String = default_logic,
    1.30 +    output: Path = Path.explode(default_output()))
    1.31 +  {
    1.32 +    val keywords = Build.outer_syntax(options, session_dirs, session_name).keywords
    1.33 +
    1.34 +    val (minor_keywords, operators) =
    1.35 +      keywords.minor.iterator.toList.partition(Symbol.is_ascii_identifier(_))
    1.36 +
    1.37 +    def major_keywords(pred: String => Boolean): List[String] =
    1.38 +      (for {
    1.39 +        k <- keywords.major.iterator
    1.40 +        kind <- keywords.kinds.get(k)
    1.41 +        if pred(kind)
    1.42 +      } yield k).toList
    1.43 +
    1.44 +    val keywords1 =
    1.45 +      major_keywords(k => k != Keyword.THY_END && k != Keyword.PRF_ASM && k != Keyword.PRF_ASM_GOAL)
    1.46 +    val keywords2 = major_keywords(Set(Keyword.THY_END))
    1.47 +    val keywords3 = major_keywords(Set(Keyword.PRF_ASM, Keyword.PRF_ASM_GOAL))
    1.48 +
    1.49 +
    1.50 +    def quote_name(a: String): String =
    1.51 +      if (Symbol.is_ascii_identifier(a)) a else "\\Q" + a + "\\E"
    1.52 +
    1.53 +    def grouped_names(as: List[String]): String =
    1.54 +      JSON.Format("\\b(" + as.sorted.map(quote_name(_)).mkString("|") + ")\\b")
    1.55 +
    1.56 +    File.write(output, """{
    1.57 +  "name": "Isabelle",
    1.58 +  "scopeName": "source.isabelle",
    1.59 +  "fileTypes": ["thy"],
    1.60 +  "uuid": "fb16e918-d05b-11e6-918e-2bb94aa2c605",
    1.61 +  "repository": {
    1.62 +    "comments": {
    1.63 +      "patterns": [
    1.64 +        {
    1.65 +          "name": "comment.block.isabelle",
    1.66 +          "begin": "\\(\\*",
    1.67 +          "beginCaptures": {
    1.68 +            "0": { "name": "punctuation.definition.comment.begin.isabelle" }
    1.69 +          },
    1.70 +          "patterns": [{ "include": "#comments" }],
    1.71 +          "end": "\\*\\)",
    1.72 +          "endCaptures": {
    1.73 +            "0": { "name": "punctuation.definition.comment.end.isabelle" }
    1.74 +          }
    1.75 +        }
    1.76 +      ]
    1.77 +    }
    1.78 +  },
    1.79 +  "patterns": [
    1.80 +    {
    1.81 +      "include": "#comments"
    1.82 +    },
    1.83 +    {
    1.84 +      "name": "keyword.control.isabelle",
    1.85 +      "match": """ + grouped_names(keywords1) + """
    1.86 +    },
    1.87 +    {
    1.88 +      "name": "keyword.other.isabelle",
    1.89 +      "match": """ + grouped_names(keywords2) + """
    1.90 +    },
    1.91 +    {
    1.92 +      "name": "keyword.operator.isabelle",
    1.93 +      "match": """ + grouped_names(operators) + """
    1.94 +    },
    1.95 +    {
    1.96 +      "name": "constant.language.isabelle",
    1.97 +      "match": """ + grouped_names(keywords3) + """
    1.98 +    },
    1.99 +    {
   1.100 +      "match": "\\b\\d*\\.?\\d+\\b",
   1.101 +      "name": "constant.numeric.isabelle"
   1.102 +    },
   1.103 +    {
   1.104 +      "name": "string.quoted.double.isabelle",
   1.105 +      "begin": "\"",
   1.106 +      "beginCaptures": {
   1.107 +        "0": { "name": "punctuation.definition.string.begin.isabelle" }
   1.108 +      },
   1.109 +      "patterns": [
   1.110 +        {
   1.111 +          "match": "\\\\.",
   1.112 +          "name": "constant.character.escape.isabelle"
   1.113 +        }
   1.114 +      ],
   1.115 +      "end": "\"",
   1.116 +      "endCaptures": {
   1.117 +        "0": { "name": "punctuation.definition.string.end.isabelle" }
   1.118 +      }
   1.119 +    }
   1.120 +  ]
   1.121 +}
   1.122 +""")
   1.123 +  }
   1.124 +
   1.125 +
   1.126 +  /* Isabelle tool wrapper */
   1.127 +
   1.128 +  val isabelle_tool = Isabelle_Tool("vscode_grammar",
   1.129 +    "generate static TextMate grammar for VSCode editor", args =>
   1.130 +  {
   1.131 +    var dirs: List[Path] = Nil
   1.132 +    var logic = default_logic
   1.133 +    var output: Option[Path] = None
   1.134 +
   1.135 +    val getopts = Getopts("""
   1.136 +Usage: isabelle vscode_grammar [OPTIONS]
   1.137 +
   1.138 +  Options are:
   1.139 +    -d DIR       include session directory
   1.140 +    -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(default_logic) + """)
   1.141 +    -o FILE      output file name (default """ + default_output() + """)
   1.142 +
   1.143 +  Generate static TextMate grammar for VSCode editor.
   1.144 +""",
   1.145 +      "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
   1.146 +      "l:" -> (arg => logic = arg),
   1.147 +      "o:" -> (arg => output = Some(Path.explode(arg))))
   1.148 +
   1.149 +    val more_args = getopts(args)
   1.150 +    if (more_args.nonEmpty) getopts.usage()
   1.151 +
   1.152 +    val output_path = output getOrElse Path.explode(default_output(logic))
   1.153 +    Output.writeln(output_path.implode)
   1.154 +
   1.155 +    generate(Options.init(), dirs, logic, output_path)
   1.156 +  })
   1.157 +}