src/Pure/General/position.scala
changeset 27968 85b5f024d94b
child 27989 a4fdc97cd2ff
equal deleted inserted replaced
27967:4a34af0f8cee 27968:85b5f024d94b
       
     1 /*  Title:      Pure/General/position.scala
       
     2     ID:         $Id$
       
     3     Author:     Makarius
       
     4 
       
     5 Position properties.
       
     6 */
       
     7 
       
     8 package isabelle
       
     9 
       
    10 import java.util.Properties
       
    11 
       
    12 
       
    13 object Position {
       
    14 
       
    15   private def get_string(name: String, props: Properties) = {
       
    16     val value = props.getProperty(name)
       
    17     if (value != null) Some(value) else None
       
    18   }
       
    19 
       
    20   private def get_int(name: String, props: Properties) = {
       
    21     get_string(name, props) match {
       
    22       case None => None
       
    23       case Some(value) =>
       
    24         try { Some(Integer.parseInt(value)) }
       
    25         catch { case e: NumberFormatException => None }
       
    26     }
       
    27   }
       
    28 
       
    29   def line_of(props: Properties) = get_int(Markup.LINE, props)
       
    30   def column_of(props: Properties) = get_int(Markup.COLUMN, props)
       
    31   def offset_of(props: Properties) = get_int(Markup.OFFSET, props)
       
    32   def end_line_of(props: Properties) = get_int(Markup.END_LINE, props)
       
    33   def end_column_of(props: Properties) = get_int(Markup.END_COLUMN, props)
       
    34   def end_offset_of(props: Properties) = get_int(Markup.END_OFFSET, props)
       
    35   def file_of(props: Properties) = get_string(Markup.FILE, props)
       
    36   def id_of(props: Properties) = get_string(Markup.ID, props)
       
    37 }