remove string interpolations (more canonical);

isabelle-prover · May 27, 2024 · c6ad324 · c6ad324
1 parent 3c13800
commit c6ad324
Show file tree

Hide file tree

Showing 5 changed files with 15 additions and 15 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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))
       }