tuned signature -- avoid warnings;
authorwenzelm
Wed, 22 Apr 2020 17:52:14 +0200
changeset 71781 3fd54f7f52b0
parent 71780 21adf2ed442c
child 71782 a57035ae9029
tuned signature -- avoid warnings;
src/Pure/General/pretty.scala
src/Pure/term.scala
--- a/src/Pure/General/pretty.scala	Wed Apr 22 13:45:02 2020 +0200
+++ b/src/Pure/General/pretty.scala	Wed Apr 22 17:52:14 2020 +0200
@@ -76,7 +76,7 @@
       val (line, rest) =
         Library.take_prefix[Tree]({ case Break(true, _, _) => false case _ => true }, prts)
       val len1 = ((0.0 /: line) { case (l, t) => l + t.length }) max len
-      rest match {
+      (rest: @unchecked) match {
         case Break(true, _, ind) :: rest1 =>
           body_length(Break(false, indent1 + ind, 0) :: rest1, len1)
         case Nil => len1
--- a/src/Pure/term.scala	Wed Apr 22 13:45:02 2020 +0200
+++ b/src/Pure/term.scala	Wed Apr 22 17:52:14 2020 +0200
@@ -195,7 +195,7 @@
         lookup(x) match {
           case Some(y) => y
           case None =>
-            x match {
+            (x: @unchecked) match {
               case PBound(_) => store(x)
               case Abst(name, typ, body) =>
                 store(Abst(cache_string(name), cache_typ(typ), cache_proof(body)))