/*  Title:      Tools/VSCode/src/grammar.scala

     Author:     Makarius

 Generate static TextMate grammar for VSCode editor.

 */

 package isabelle.vscode

 import isabelle._

 import java.util.UUID

 object Grammar

 {

   /* generate grammar */

   private lazy val default_logic = Isabelle_System.getenv("ISABELLE_LOGIC")

   private 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 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")

     """{

   "name": "Isabelle",

   "scopeName": "source.isabelle",

   "fileTypes": ["thy"],

   "uuid": """ + JSON.Format(UUID.randomUUID().toString) + """,

   "repository": {

     "comment": {

       "patterns": [

         {

           "name": "comment.block.isabelle",

           "begin": "\\(\\*",

           "beginCaptures": {

             "0": { "name": "punctuation.definition.comment.begin.isabelle" }

           },

           "patterns": [{ "include": "#comment" }],

           "end": "\\*\\)",

           "endCaptures": {

             "0": { "name": "punctuation.definition.comment.end.isabelle" }

           }

         }

       ]

     },

     "cartouche": {

       "patterns": [

         {

           "name": "string.quoted.other.multiline.isabelle",

           "begin": "(?:\\\\<open>|‹)",

           "beginCaptures": {

             "0": { "name": "punctuation.definition.string.begin.isabelle" }

           },

           "patterns": [{ "include": "#cartouche" }],

           "end": "(?:\\\\<close>|›)",

           "endCaptures": {

             "0": { "name": "punctuation.definition.string.end.isabelle" }

           }

         }

       ]

     }

   },

   "patterns": [

     {

       "include": "#comment"

     },

     {

       "include": "#cartouche"

     },

     {

       "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": """ + JSON.Format("""\\[\"]|\\\d\d\d""") + """,

           "name": "constant.character.escape.isabelle"

         }

       ],

       "end": "\"",

       "endCaptures": {

         "0": { "name": "punctuation.definition.string.end.isabelle" }

       }

     },

     {

       "name": "string.quoted.backtick.isabelle",

       "begin": "`",

       "beginCaptures": {

         "0": { "name": "punctuation.definition.string.begin.isabelle" }

       },

       "patterns": [

         {

           "match": """ + JSON.Format("""\\[\`]|\\\d\d\d""") + """,

           "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 keywords = Build.outer_syntax(Options.init(), dirs, logic).keywords

     val output_path = output getOrElse Path.explode(default_output(logic))

     Output.writeln(output_path.implode)

     File.write_backup(output_path, generate(keywords))

   })

 }