src/Pure/General/position.scala

Reintroduce set_interpreter for Collect and op :.
I removed them by accident when removing old code that dealt with the "set" type.
Incidentally, there is still some broken "set" code in Refute that should be fixed (see TODO in refute.ML).

/*  Title:      Pure/General/position.scala
    Author:     Makarius

Position properties.
*/

package isabelle

import java.util.Properties


object Position {

  private def get_string(name: String, props: Properties) = {
    val value = if (props != null) props.getProperty(name) else null
    if (value != null) Some(value) else None
  }

  private def get_int(name: String, props: Properties) = {
    get_string(name, props) match {
      case None => None
      case Some(value) =>
        try { Some(Integer.parseInt(value)) }
        catch { case _: NumberFormatException => None }
    }
  }

  def line_of(props: Properties) = get_int(Markup.LINE, props)
  def column_of(props: Properties) = get_int(Markup.COLUMN, props)
  def offset_of(props: Properties) = get_int(Markup.OFFSET, props)
  def end_line_of(props: Properties) = get_int(Markup.END_LINE, props)
  def end_column_of(props: Properties) = get_int(Markup.END_COLUMN, props)
  def end_offset_of(props: Properties) = get_int(Markup.END_OFFSET, props)
  def file_of(props: Properties) = get_string(Markup.FILE, props)
  def id_of(props: Properties) = get_string(Markup.ID, props)
}