# HG changeset patch # User wenzelm # Date 1610120180 -3600 # Node ID 578a33042aa6c6a6e7b300f3fe62f53d0cb06e1a # Parent 87067698ae53d5e97f95ffbd370d3408a9ccd964 clarified: command keyword position is sufficient (amending 693a39f2cddc); diff -r 87067698ae53 -r 578a33042aa6 src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML Fri Jan 08 15:13:23 2021 +0100 +++ b/src/Pure/PIDE/command.ML Fri Jan 08 16:36:20 2021 +0100 @@ -243,10 +243,8 @@ NONE => () | SOME 0 => () | SOME n => - let - val pos = #1 (Toplevel.body_range_of tr); - val m = Markup.command_indent (n - 1); - in Toplevel.setmp_thread_position tr (fn () => Position.report pos m) () end) + let val report = Markup.markup_only (Markup.command_indent (n - 1)); + in Toplevel.setmp_thread_position tr (fn () => Output.report [report]) () end) else () end | NONE => ()); diff -r 87067698ae53 -r 578a33042aa6 src/Tools/jEdit/src/text_structure.scala --- a/src/Tools/jEdit/src/text_structure.scala Fri Jan 08 15:13:23 2021 +0100 +++ b/src/Tools/jEdit/src/text_structure.scala Fri Jan 08 16:36:20 2021 +0100 @@ -146,7 +146,8 @@ else if (Token_Markup.Line_Context.after(buffer, current_line).structure.blank) 0 else { line_head(current_line) match { - case Some(info @ Text.Info(range, tok)) => + case Some(info) => + val tok = info.info if (tok.is_begin || keywords.is_before_command(tok) || keywords.is_command(tok, Keyword.theory)) 0