src/Tools/jEdit/src/token_markup.scala
changeset 53277 6aa348237973
parent 53274 1760c01f1c78
child 53278 c31532691e55
equal deleted inserted replaced
53276:cbed0aa0b0db 53277:6aa348237973
   204         case other: Line_Context => context == other.context
   204         case other: Line_Context => context == other.context
   205         case _ => false
   205         case _ => false
   206       }
   206       }
   207   }
   207   }
   208 
   208 
   209   class Marker(ext_styles: Boolean, get_syntax: => Option[Outer_Syntax]) extends TokenMarker
   209   class Marker(mode: String) extends TokenMarker
   210   {
   210   {
       
   211     private val ext_styles = mode == "isabelle"
       
   212 
   211     override def markTokens(context: TokenMarker.LineContext,
   213     override def markTokens(context: TokenMarker.LineContext,
   212         handler: TokenHandler, raw_line: Segment): TokenMarker.LineContext =
   214         handler: TokenHandler, raw_line: Segment): TokenMarker.LineContext =
   213     {
   215     {
   214       val line_ctxt =
   216       val line_ctxt =
   215         context match {
   217         context match {
   218         }
   220         }
   219       val line = if (raw_line == null) new Segment else raw_line
   221       val line = if (raw_line == null) new Segment else raw_line
   220 
   222 
   221       val context1 =
   223       val context1 =
   222       {
   224       {
   223         val syntax = get_syntax
   225         val syntax = Isabelle.mode_syntax(mode)
   224         val (styled_tokens, context1) =
   226         val (styled_tokens, context1) =
   225           if (line_ctxt.isDefined && syntax.isDefined) {
   227           if (line_ctxt.isDefined && syntax.isDefined) {
   226             val (tokens, ctxt1) = syntax.get.scan_context(line, line_ctxt.get)
   228             val (tokens, ctxt1) = syntax.get.scan_context(line, line_ctxt.get)
   227             val styled_tokens = tokens.map(tok => (Rendering.token_markup(syntax.get, tok), tok))
   229             val styled_tokens = tokens.map(tok => (Rendering.token_markup(syntax.get, tok), tok))
   228             (styled_tokens, new Line_Context(Some(ctxt1)))
   230             (styled_tokens, new Line_Context(Some(ctxt1)))
   264   }
   266   }
   265 
   267 
   266 
   268 
   267   /* mode provider */
   269   /* mode provider */
   268 
   270 
   269   private val markers = Map(
       
   270     "isabelle" -> new Token_Markup.Marker(true, PIDE.get_recent_syntax()),
       
   271     "isabelle-options" -> new Token_Markup.Marker(false, Some(Options.options_syntax)),
       
   272     "isabelle-root" -> new Token_Markup.Marker(false, Some(Build.root_syntax)))
       
   273 
       
   274   class Mode_Provider(orig_provider: ModeProvider) extends ModeProvider
   271   class Mode_Provider(orig_provider: ModeProvider) extends ModeProvider
   275   {
   272   {
   276     for (mode <- orig_provider.getModes) addMode(mode)
   273     for (mode <- orig_provider.getModes) addMode(mode)
   277 
   274 
   278     override def loadMode(mode: Mode, xmh: XModeHandler)
   275     override def loadMode(mode: Mode, xmh: XModeHandler)
   279     {
   276     {
   280       super.loadMode(mode, xmh)
   277       super.loadMode(mode, xmh)
   281       markers.get(mode.getName).map(mode.setTokenMarker(_))
   278       Isabelle.token_marker(mode.getName).foreach(mode.setTokenMarker _)
   282     }
   279     }
   283   }
   280   }
   284 
   281 
   285   def refresh_buffer(buffer: JEditBuffer)
   282   def refresh_buffer(buffer: JEditBuffer)
   286   {
   283   {
   287     buffer.setTokenMarker(jEdit.getMode("text").getTokenMarker)
   284     Isabelle.token_marker(JEdit_Lib.buffer_mode(buffer)) match {
   288     val marker = markers.get(JEdit_Lib.buffer_mode(buffer))
   285       case None =>
   289     marker.map(buffer.setTokenMarker(_))
   286       case Some(marker) =>
       
   287         buffer.setTokenMarker(jEdit.getMode("text").getTokenMarker)
       
   288         buffer.setTokenMarker(marker)
       
   289     }
   290   }
   290   }
   291 }
   291 }
   292 
   292