src/Pure/General/position.scala
changeset 27993 6dd90ef9f927
parent 27989 a4fdc97cd2ff
child 29140 e7ac5bb20aed
equal deleted inserted replaced
27992:131f7ea9e6e6 27993:6dd90ef9f927
    20   private def get_int(name: String, props: Properties) = {
    20   private def get_int(name: String, props: Properties) = {
    21     get_string(name, props) match {
    21     get_string(name, props) match {
    22       case None => None
    22       case None => None
    23       case Some(value) =>
    23       case Some(value) =>
    24         try { Some(Integer.parseInt(value)) }
    24         try { Some(Integer.parseInt(value)) }
    25         catch { case e: NumberFormatException => None }
    25         catch { case _: NumberFormatException => None }
    26     }
    26     }
    27   }
    27   }
    28 
    28 
    29   def line_of(props: Properties) = get_int(Markup.LINE, props)
    29   def line_of(props: Properties) = get_int(Markup.LINE, props)
    30   def column_of(props: Properties) = get_int(Markup.COLUMN, props)
    30   def column_of(props: Properties) = get_int(Markup.COLUMN, props)