# HG changeset patch # User wenzelm # Date 1377774840 -7200 # Node ID cbed0aa0b0db6f7fd8ff278c7db8380d6f297b22 # Parent b34aac6511aba83af9bcf3001c15adee0f0f5c38 syntax for isabelle-news with symbol completion; diff -r b34aac6511ab -r cbed0aa0b0db src/Tools/jEdit/src/isabelle.scala --- a/src/Tools/jEdit/src/isabelle.scala Thu Aug 29 13:00:59 2013 +0200 +++ b/src/Tools/jEdit/src/isabelle.scala Thu Aug 29 13:14:00 2013 +0200 @@ -20,12 +20,14 @@ val modes = List("isabelle", "isabelle-options", "isabelle-root", "isabelle-news") + private lazy val news_syntax = Outer_Syntax.init() + def mode_syntax(name: String): Option[Outer_Syntax] = name match { case "isabelle" | "isabelle-raw" => PIDE.get_recent_syntax case "isabelle-options" => Some(Options.options_syntax) case "isabelle-root" => Some(Build.root_syntax) - case "isabelle-news" => Some(Outer_Syntax.empty) + case "isabelle-news" => Some(news_syntax) case _ => None }