tuned;
authorwenzelm
Mon Jan 02 09:27:33 2017 +0100 (2017-01-02)
changeset 6474117bd2947a822
parent 64740 01af31db2720
child 64742 5f946e8887c5
tuned;
src/Tools/VSCode/src/grammar.scala
     1.1 --- a/src/Tools/VSCode/src/grammar.scala	Sun Jan 01 23:56:36 2017 +0100
     1.2 +++ b/src/Tools/VSCode/src/grammar.scala	Mon Jan 02 09:27:33 2017 +0100
     1.3 @@ -19,17 +19,11 @@
     1.4    private lazy val default_logic = Isabelle_System.getenv("ISABELLE_LOGIC")
     1.5  
     1.6    private def default_output(logic: String = ""): String =
     1.7 -    if (logic == default_logic) "isabelle-grammar.json"
     1.8 +    if (logic == "" || logic == default_logic) "isabelle-grammar.json"
     1.9      else "isabelle-" + logic + "-grammar.json"
    1.10  
    1.11 -  def generate(
    1.12 -    options: Options,
    1.13 -    session_dirs: List[Path] = Nil,
    1.14 -    session_name: String = default_logic,
    1.15 -    output: Path = Path.explode(default_output()))
    1.16 +  def generate(keywords: Keyword.Keywords): JSON.S =
    1.17    {
    1.18 -    val keywords = Build.outer_syntax(options, session_dirs, session_name).keywords
    1.19 -
    1.20      val (minor_keywords, operators) =
    1.21        keywords.minor.iterator.toList.partition(Symbol.is_ascii_identifier(_))
    1.22  
    1.23 @@ -52,7 +46,7 @@
    1.24      def grouped_names(as: List[String]): String =
    1.25        JSON.Format("\\b(" + as.sorted.map(quote_name(_)).mkString("|") + ")\\b")
    1.26  
    1.27 -    File.write(output, """{
    1.28 +    """{
    1.29    "name": "Isabelle",
    1.30    "scopeName": "source.isabelle",
    1.31    "fileTypes": ["thy"],
    1.32 @@ -118,7 +112,7 @@
    1.33      }
    1.34    ]
    1.35  }
    1.36 -""")
    1.37 +"""
    1.38    }
    1.39  
    1.40  
    1.41 @@ -148,9 +142,10 @@
    1.42      val more_args = getopts(args)
    1.43      if (more_args.nonEmpty) getopts.usage()
    1.44  
    1.45 +    val keywords = Build.outer_syntax(Options.init(), dirs, logic).keywords
    1.46      val output_path = output getOrElse Path.explode(default_output(logic))
    1.47 +
    1.48      Output.writeln(output_path.implode)
    1.49 -
    1.50 -    generate(Options.init(), dirs, logic, output_path)
    1.51 +    File.write(output_path, generate(keywords))
    1.52    })
    1.53  }