# HG changeset patch # User wenzelm # Date 1483345653 -3600 # Node ID 17bd2947a82276753172d374409da92952340e7f # Parent 01af31db27200290375b7e507a953ef7f8d895d6 tuned; diff -r 01af31db2720 -r 17bd2947a822 src/Tools/VSCode/src/grammar.scala --- a/src/Tools/VSCode/src/grammar.scala Sun Jan 01 23:56:36 2017 +0100 +++ b/src/Tools/VSCode/src/grammar.scala Mon Jan 02 09:27:33 2017 +0100 @@ -19,17 +19,11 @@ private lazy val default_logic = Isabelle_System.getenv("ISABELLE_LOGIC") private def default_output(logic: String = ""): String = - if (logic == default_logic) "isabelle-grammar.json" + if (logic == "" || 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())) + def generate(keywords: Keyword.Keywords): JSON.S = { - val keywords = Build.outer_syntax(options, session_dirs, session_name).keywords - val (minor_keywords, operators) = keywords.minor.iterator.toList.partition(Symbol.is_ascii_identifier(_)) @@ -52,7 +46,7 @@ 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"], @@ -118,7 +112,7 @@ } ] } -""") +""" } @@ -148,9 +142,10 @@ 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) - - generate(Options.init(), dirs, logic, output_path) + File.write(output_path, generate(keywords)) }) }