remove custom markup (including edits): hack does not work any more i…

…n current JDK;

jedit_linter/etc/build.props

@@ -5,7 +5,6 @@ requirements = \
   env:JEDIT_JARS \
   env:ISABELLE_LINTER_JAR
 sources = \
-  src/Handle.java \
   src/jedit_extension.scala \
   src/jedit_linter_plugin.scala \
   src/linter_dockable.scala \

jedit_linter/src/jedit_extension.scala

@@ -18,27 +18,6 @@ import org.gjt.sp.jedit.textarea.TextArea
 
 // FIXME this should be code in upstream / unnecessary
 object JEdit_Extension {
-  private val handle: VarHandle = {
-    val lookup = MethodHandles.privateLookupIn(classOf[Field], MethodHandles.lookup)
-    lookup.findVarHandle(classOf[Field], "modifiers", classOf[Int])
-  }
-
-  private def remove_final(field: Field) = {
-    field.setAccessible(true)
-    val mods = field.getModifiers & ~Modifier.FINAL
-    Handle.set_modifiers(handle, field, mods)
-    field
-  }
-
-  def init: Unit = {
-    val ext_elements = Markup.Elements(Linter_Markup.LINTER_SENDBACK, Linter_Markup.GOTO_POSITION)
-
-    val active_elements = Rendering.getClass.getDeclaredField("active_elements")
-    remove_final(active_elements).set(Rendering, Rendering.active_elements ++ ext_elements)
-    val background_elements = Rendering.getClass.getDeclaredField("background_elements")
-    remove_final(background_elements).set(Rendering, Rendering.background_elements ++ ext_elements)
-  }
-
   def load_linter_thy(): Unit = {
     val path = Path.explode("$JEDIT_LINTER_HOME/Linter.thy").canonical
 
@@ -51,44 +30,4 @@ object JEdit_Extension {
       Document_Model.node_required(node_name, set = true)
     }
   }
-
-  def replace_range(
-    snapshot: Document.Snapshot,
-    text_area: TextArea,
-    range: Symbol.Range, text: String
-  ): Unit = {
-    val buffer = text_area.getBuffer
-    if (!snapshot.is_outdated) {
-      JEdit_Lib.buffer_edit(buffer) {
-        text_area.moveCaretPosition(range.start + range.length)
-        val start_line = text_area.getCaretLine + 1
-        text_area.setSelectedText(text)
-        val end_line = text_area.getCaretLine
-        for (line <- start_line to end_line) {
-          Token_Markup.Line_Context.refresh(buffer, line)
-          buffer.indentLine(line, true)
-        }
-        buffer.remove(range.start, range.length)
-      }
-    }
-  }
-
-  class Handler extends Active.Handler {
-    override def handle(view: View, text: String, elem: XML.Elem,
-      doc_view: Document_View, snapshot: Document.Snapshot): Boolean = {
-      elem match {
-        case XML.Elem(Markup(Linter_Markup.LINTER_SENDBACK, props), _) =>
-          for {
-            range <- Position.Range.unapply(props)
-            replacement <- Markup.Content.unapply(props)
-          } replace_range(snapshot, doc_view.text_area, range, replacement)
-          true
-        case XML.Elem(Markup(Linter_Markup.GOTO_POSITION, pos), _) =>
-          val link = PIDE.editor.hyperlink_position(true, snapshot, pos)
-          GUI_Thread.later { link.foreach(_.follow(view)) }
-          true
-        case _ => false
-      }
-    }
-  }
 }

jedit_linter/src/linter_overlay.scala

@@ -67,14 +67,8 @@ object Linter_Overlay {
       {
         val res = results.map(_._2).flatMap { result =>
           val level = result.severity.toString
-          val edit = result.edit match {
-            case Some(edit) =>
-              XML_Presenter.text("\n  Consider: ") ::: XML_Presenter.edit_markup(edit)
-            case None =>
-              Nil
-          }
           val text = XML_Presenter.text(s"${result.message} (${result.lint_name})")
-          val body = XML_Presenter.add_meta(text ::: edit, result)
+          val body = XML_Presenter.add_meta(text, result)
           level :: body.map(XML.string_of_tree)
         }
 

jedit_linter/src/linter_plugin.scala

@@ -13,8 +13,6 @@ import org.gjt.sp.jedit.{EBMessage, EBPlugin}
 
 
 class Linter_Plugin extends EBPlugin {
-  JEdit_Extension.init
-
   val linter = new Linter_Variable()
   val overlays = new Linter_Overlay.Variable
   private var shutdown = false

linter_base/src/lint.scala

@@ -35,20 +35,18 @@ abstract class Proper_Commands_Lint(val name: String, val severity: Severity.Lev
   def add_result(
     message: String,
     range: Text.Range,
-    edit: Option[Edit],
     command: Parsed_Command,
     report: Report
   ): Report =
-    report + Result(name, message, range, edit, severity, command, short_description)
+    report + Result(name, message, range, severity, command, short_description)
 
   def add_result(
     message: String,
     range: Text.Range,
-    edit: Option[Edit],
     commands: List[Parsed_Command],
     report: Report
   ): Report =
-    report + Result(name, message, range, edit, severity, commands, short_description)
+    report + Result(name, message, range, severity, commands, short_description)
 }
 
 abstract class Single_Command_Lint(val name: String, val severity: Severity.Level) extends Lint {

linter_base/src/linter.scala

@@ -21,7 +21,6 @@ object Linter {
     lint_name: String,
     message: String,
     range: Text.Range,
-    edit: Option[Edit],
     severity: Severity.Value,
     commands: List[Parsed_Command],
     short_description: Lint_Description
@@ -37,11 +36,10 @@ object Linter {
       lint_name: String,
       message: String,
       range: Text.Range,
-      edit: Option[Edit],
       severity: Severity.Value,
       command: Parsed_Command,
       short_description: Lint_Description): Result =
-      Result(lint_name, message, range, edit, severity, command :: Nil, short_description)
+      Result(lint_name, message, range, severity, command :: Nil, short_description)
   }
   object Report {
     def init(name: Document.Node.Name): Report = new Report(name, Nil)
@@ -64,18 +62,14 @@ object Linter {
         .sortBy(_.info.id) // Lowest severity first
   }
 
-  case class Edit(range: Text.Range, replacement: String, msg: Option[String] = None) {
-    val message: String = msg.getOrElse(replacement)
-  }
-
   case class Reporter(
     command: Parsed_Command,
     name: String,
     severity: Severity.Level,
     short_description: Lint_Description
   ) {
-    def apply(message: String, range: Text.Range, edit: Option[Edit]): Some[Result] =
-      Some(Result(name, message, range, edit, severity, command, short_description))
+    def apply(message: String, range: Text.Range): Some[Result] =
+      Some(Result(name, message, range, severity, command, short_description))
 
     def source(range: Text.Range): String = command.source(range)
   }

linter_base/src/lints.scala

@@ -35,7 +35,6 @@ object Lints {
           val new_report = add_result(
             "Do not switch between apply-style and ISAR proofs.",
             proof.range,
-            None,
             proof,
             report)
           lint_proper(next, new_report)
@@ -71,7 +70,7 @@ object Lints {
           val apply1 = s"apply ${report.source(method1.range)}\n"
           val apply2 = method2.map(some_method => s"apply ${report.source(some_method.range)}\n").getOrElse("")
           val replacement = apply1 + apply2 + "done"
-          report("Use \"apply\" instead of \"by\".", proof.range, Some(Edit(proof.range, replacement)))
+          report("Use \"apply\" instead of \"by\".", proof.range)
         case _ => None
       }
   })
@@ -140,7 +139,6 @@ object Lints {
       } yield add_result(
         """Use "by" instead of a short apply-script.""",
         Parsers.list_range(apply_script.map(_.range)),
-        Some(Edit(Parsers.list_range(apply_script map (_.range)), replacement)),
         apply_script,
         report)
       new_report.getOrElse(report)
@@ -216,7 +214,7 @@ object Lints {
 
     private def report_lint(apply: Parsed_Command, report: Report): Report =
       add_result("Do not use unrestricted auto as a non-terminal proof method.", apply.range,
-        None, apply, report)
+        apply, report)
 
     @tailrec
     def lint_proper(commands: List[Parsed_Command], report: Report): Report =
@@ -267,7 +265,6 @@ object Lints {
           add_result(
             "Compress low-level proof methods into automated search.",
             Parsers.list_range(low_level_commands.map(_.range)),
-            None,
             low_level_commands,
             report)
         }
@@ -332,7 +329,6 @@ object Lints {
           add_result(
             "Use context or bundles instead of global simp attribute changes.",
             command.range,
-            None,
             command,
             report)
         }
@@ -382,7 +378,7 @@ object Lints {
 
     def lint(command: Parsed_Command, report: Reporter): Option[Result] = command match {
       case c@Parsed_Command("apply") =>
-        report("Use Isar instead of apply-scripts.", c.range, None)
+        report("Use Isar instead of apply-scripts.", c.range)
       case _ => None
     }
   })
@@ -417,8 +413,7 @@ object Lints {
           case xs@_ :: _ =>
             report(
               """Do not use axiomatization with a where clause.""",
-              Text.Range(xs.head.range.start, xs.last.range.stop),
-              Some(Edit(Parsers.list_range(xs.map(_.range)), "", Some("Remove where"))))
+              Text.Range(xs.head.range.start, xs.last.range.stop))
           case Nil => None
         }
       case _ => None
@@ -444,8 +439,7 @@ object Lints {
     }
 
     def lint(command: Parsed_Command, report: Reporter): Option[Result] =
-      if (illegal_commands.contains(command.kind))
-        report(message, command.range, Some(Edit(command.range, "", Some("Remove invocation"))))
+      if (illegal_commands.contains(command.kind)) report(message, command.range)
       else None
   }
 
@@ -472,7 +466,7 @@ object Lints {
           _.find(is_smt_oracle) match {
             case None => failure("no match")
             case Some(tokens) =>
-              success(report("Do not use smt_oracle.", tokens.head.range, None))
+              success(report("Do not use smt_oracle.", tokens.head.range))
           }
         }))
   })
@@ -528,10 +522,7 @@ object Lints {
     override def lint_ast_node(elem: Text.Info[AST_Node], report: Reporter): Option[Result] =
       elem.info match {
         case Counter_Example_Finder(_, attributes) if attributes.isEmpty || no_expect(attributes)
-        => report(
-          "Remove counter-example finder command.",
-          elem.range,
-          Some(Edit(elem.range, "", Some("Remove invocation"))))
+        => report("Remove counter-example finder command.", elem.range)
         case _ => None
       }
   })
@@ -548,7 +539,7 @@ object Lints {
       p_command("fun", "primrec", "abbreviation", "definition", "inductive", "inductive_set") ~>
         elem("ident", t => t.info.is_ident && t.info.content.length < 2) ^^ {
           case Text.Info(range, token) =>
-            report(s"""Name "${token.content}" is too short.""", range, None)
+            report(s"""Name "${token.content}" is too short.""", range)
         }
   })
 
@@ -584,7 +575,7 @@ object Lints {
 
     override def parser(reporter: Reporter): Parser[Some[Result]] = {
       def report(attr: Elem): Parser[Some[Result]] =
-        success(reporter("Do not use global attributes on unnamed lemmas.", attr.range, None))
+        success(reporter("Do not use global attributes on unnamed lemmas.", attr.range))
 
       ((p_command("lemma", "theorem", "corollary") ~> p_attr) ~
         (p_atom(t => !t.is_keyword("shows")).* ~> p_show.*)) >> {
@@ -622,7 +613,7 @@ object Lints {
     override def lint_method(method: Text.Info[Method], report: Reporter): Option[Result] =
       method.info match {
         case Simple_Method(RToken(_, name, _), _, _) if TACTICS.contains(name) =>
-          report("Do not use tactic proofs.", method.range, None)
+          report("Do not use tactic proofs.", method.range)
         case Combined_Method(left, _, right, _) =>
           lint_method(left, report).orElse(lint_method(right, report))
         case _ => None
@@ -654,7 +645,7 @@ object Lints {
         _.find(simp_or_cong) match {
           case None => failure("no match")
           case Some(tokens) =>
-            success(report("Do not use transforming attributes on lemmas.", tokens.head.range, None))
+            success(report("Do not use transforming attributes on lemmas.", tokens.head.range))
         }
       }
   })
@@ -678,7 +669,7 @@ object Lints {
     override def lint_method(method: Text.Info[Method], report: Reporter): Option[Result] =
       method.info match {
         case Simple_Method(RToken(_, "rule", _), _, Nil) =>
-          report("Do not use implicit rule.", method.range, None)
+          report("Do not use implicit rule.", method.range)
         case Combined_Method(left, _, right, _) =>
           lint_method(left, report) orElse lint_method(right, report)
         case _ => None
@@ -743,7 +734,7 @@ object Lints {
       for {
         Text.Info(range, s_method) <- method
         if is_complex_method(s_method)
-      } yield report("Keep initial proof methods simple.", range, None).get
+      } yield report("Keep initial proof methods simple.", range).get
   })
 
   val simplifier_isar_initial_method = Lint_Wrapper("simplifier_isar_initial_method",
@@ -775,7 +766,7 @@ object Lints {
         for {
           Text.Info(range, s_method) <- method
           if calls_simplifier(s_method)
-        } yield report("Do not use simplifier as initial proof methods.", range, None).get
+        } yield report("Do not use simplifier as initial proof methods.", range).get
     })
 
   val force_failure = Lint_Wrapper("force_failure",
@@ -797,7 +788,7 @@ object Lints {
     override def lint_method(method: Text.Info[Method], report: Reporter): Option[Result] =
       method.info match {
         case Simple_Method(RToken(_, "simp", _), _, _) =>
-          report("Consider forcing failure.", method.range, None)
+          report("Consider forcing failure.", method.range)
         case _ => None
       }
   })
@@ -825,7 +816,7 @@ object Lints {
       method.info match {
         case Simple_Method(_, _, _) => None
         case Combined_Method(left, Method.Combinator.Struct, _, _) =>
-          if (has_auto(left.info)) report("Do not use apply (auto;...)", method.range, None) else None
+          if (has_auto(left.info)) report("Do not use apply (auto;...)", method.range) else None
         case Combined_Method(left, _, right, _) =>
           lint_method(left, report).orElse(lint_method(right, report))
       }
@@ -850,7 +841,7 @@ object Lints {
     val message: String = "Avoid complex methods."
 
     override def lint_method(method: Text.Info[Method], report: Reporter): Option[Result] =
-      if (is_complex_method(method.info)) report(message, method.range, None)
+      if (is_complex_method(method.info)) report(message, method.range)
       else None
   })
 
@@ -861,7 +852,7 @@ object Lints {
     val long_description: Lint_Description = short_description
 
     override def lint_ast_node(elem: Text.Info[AST_Node], report: Reporter): Option[Result] =
-      report(s"Parsed: ${elem.info}", elem.range, None)
+      report(s"Parsed: ${elem.info}", elem.range)
   })
 }
 

linter_base/src/markup.scala

@@ -10,9 +10,6 @@ import isabelle._
 
 
 object Linter_Markup {
-  val LINTER_SENDBACK = "linter_sendback"
-  val GOTO_POSITION = "goto_position"
-
   val LINT_RESULT = "lint_result"
 
   val LINT_NAME = "lint_name"