src/Tools/jEdit/src/token_markup.scala
changeset 50205 788c8263e634
parent 50199 6d04e2422769
child 50210 747db833fbf7
equal deleted inserted replaced
50204:daeb1674fb91 50205:788c8263e634
   263 
   263 
   264 
   264 
   265   /* mode provider */
   265   /* mode provider */
   266 
   266 
   267   private val markers = Map(
   267   private val markers = Map(
   268     "isabelle" -> new Token_Markup.Marker(true, Isabelle.get_recent_syntax()),
   268     "isabelle" -> new Token_Markup.Marker(true, PIDE.get_recent_syntax()),
   269     "isabelle-options" -> new Token_Markup.Marker(false, Some(Options.options_syntax)),
   269     "isabelle-options" -> new Token_Markup.Marker(false, Some(Options.options_syntax)),
   270     "isabelle-root" -> new Token_Markup.Marker(false, Some(Build.root_syntax)))
   270     "isabelle-root" -> new Token_Markup.Marker(false, Some(Build.root_syntax)))
   271 
   271 
   272   class Mode_Provider(orig_provider: ModeProvider) extends ModeProvider
   272   class Mode_Provider(orig_provider: ModeProvider) extends ModeProvider
   273   {
   273   {