src/Pure/General/position.scala
changeset 68287 2ae74a278c10
parent 67882 7eb4c966e156
child 72692 22aeec526ffd
equal deleted inserted replaced
68286:b9160ca067ae 68287:2ae74a278c10
   142           case (Some(i), None) => "line " + i.toString
   142           case (Some(i), None) => "line " + i.toString
   143           case (Some(i), Some(name)) => "line " + i.toString + " of " + quote(name)
   143           case (Some(i), Some(name)) => "line " + i.toString + " of " + quote(name)
   144           case (None, Some(name)) => "file " + quote(name)
   144           case (None, Some(name)) => "file " + quote(name)
   145           case _ => ""
   145           case _ => ""
   146         }
   146         }
   147       val s = if (s0 == "") s0 else if (delimited) " (" + s0 + ")" else " " + s0
   147       val s = if (s0 == "") s0 else if (delimited) " (" + s0 + ")" else s0
   148       Markup(Markup.POSITION, pos).markup(s)
   148       Markup(Markup.POSITION, pos).markup(s)
   149     }
   149     }
   150   }
   150   }
   151 
   151 
   152 
   152