diff --git a/jedit_linter/src/linter_overlay.scala b/jedit_linter/src/linter_overlay.scala index bce1aaf..e1a2f6b 100644 --- a/jedit_linter/src/linter_overlay.scala +++ b/jedit_linter/src/linter_overlay.scala @@ -67,7 +67,7 @@ object Linter_Overlay { { val res = results.map(_._2).flatMap { result => val level = result.severity.toString - val text = XML_Presenter.text(s"${result.message} (${result.lint_name})") + val text = XML_Presenter.text(result.message + " (" + result.lint_name + ")") val body = XML_Presenter.add_meta(text, result) level :: body.map(XML.string_of_tree) } diff --git a/linter_base/src/linter.scala b/linter_base/src/linter.scala index 9f8a7a4..ee34742 100644 --- a/linter_base/src/linter.scala +++ b/linter_base/src/linter.scala @@ -327,7 +327,7 @@ Lint isabelle theories. case "xml" => XML_Presenter case "csv" => CSV_Presenter(configuration) case "count" => Count - case _ => error(s"Unrecognized reporting mode $mode") + case _ => error("Unrecognized reporting mode " + mode) } progress.interrupt_handler { diff --git a/linter_base/src/lints.scala b/linter_base/src/lints.scala index 3f81c71..d70717c 100644 --- a/linter_base/src/lints.scala +++ b/linter_base/src/lints.scala @@ -67,8 +67,8 @@ object Lints { override def lint_proof(proof: Text.Info[Proof], report: Reporter): Option[Result] = proof.info match { case By(method1, method2) => - 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 apply1 = "apply " + report.source(method1.range) + "\n" + val apply2 = method2.map(some_method => "apply " + report.source(some_method.range) + "\n").getOrElse("") val replacement = apply1 + apply2 + "done" report("Use \"apply\" instead of \"by\".", proof.range) case _ => None @@ -115,16 +115,16 @@ object Lints { for { method1 <- try_transform(removeApply, apply1, true) method2 <- try_transform(removeApply, apply2, true) - } yield s"by $method1 $method2" + } yield "by " + method1 + " " + method2 case apply :: _ :: Nil if !has_by => for { method <- try_transform(removeApply, apply, true) - } yield s"by $method" + } yield "by " + method case apply :: by :: Nil if has_by => for { method1 <- try_transform(removeApply, apply, true) method2 <- try_transform(removeBy, by, true) - } yield s"by $method1 $method2" + } yield "by " + method1 + " " + method2 case _ => None } } @@ -539,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) + report("Name \"" + token.content + "\" is too short.", range) } }) @@ -852,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) + report("Parsed: " + elem.info, elem.range) }) } diff --git a/linter_base/src/parsers.scala b/linter_base/src/parsers.scala index bf990b5..4c9fbed 100644 --- a/linter_base/src/parsers.scala +++ b/linter_base/src/parsers.scala @@ -61,7 +61,7 @@ case class Parsed_Command( Token_Parsers.parse(Token_Parsers.token_parser, tokens) match { case Token_Parsers.Success(result, Token_Parsers.Token_Reader(Nil)) => result case Token_Parsers.Success(_, next) => - Text.Info(range, Failed(s"Failed parsing. $next left")) + Text.Info(range, Failed("Failed parsing. " + next + " left")) case failure: Token_Parsers.NoSuccess => Text.Info(range, Failed(failure.msg)) } } diff --git a/linter_base/src/presenter.scala b/linter_base/src/presenter.scala index 20ecf57..6d8cacb 100644 --- a/linter_base/src/presenter.scala +++ b/linter_base/src/presenter.scala @@ -139,15 +139,15 @@ object XML_Presenter extends Presenter[XML.Body] { show_descriptions: Boolean = false ): XML.Body = { val inner = - if (compact) text(s" ${lint_number + 1}. ${lint_result.message}") + if (compact) text(" " + (lint_number + 1) + ". " + lint_result.message) else { (position_markup(lint_result) - ::: text(s" ${lint_result.message}") - ::: text(s"\n Name: ${lint_result.lint_name}") - ::: text(s"\n Severity: ${lint_result.severity}") + ::: text(" " + lint_result.message) + ::: text("\n Name: " + lint_result.lint_name) + ::: text("\n Severity: " + lint_result.severity) ::: (if (show_descriptions) - text(s"\n Description: ") ::: + text("\n Description: ") ::: Lint_Description.XML_Presentation.render(lint_result.short_description) else Nil)) }