src/Pure/General/position.scala

 */
 
 package isabelle
 
 
-object Position
-{
+object Position {
   type T = Properties.T
 
   val none: T = Nil
 
   val Line = new Properties.Int(Markup.LINE)

   val Def_File = new Properties.String(Markup.DEF_FILE)
   val Def_Id = new Properties.Long(Markup.DEF_ID)
 
   val Def_Theory = new Properties.String(Markup.DEF_THEORY)
 
-  object Line_File
-  {
+  object Line_File {
     def apply(line: Int, file: String): T =
       (if (line > 0) Line(line) else Nil) :::
       (if (file != "") File(file) else Nil)
 
     def unapply(pos: T): Option[(Int, String)] =

         case (_, File(name)) => Some((1, name))
         case _ => None
       }
   }
 
-  object Def_Line_File
-  {
+  object Def_Line_File {
     def unapply(pos: T): Option[(Int, String)] =
       (pos, pos) match {
         case (Def_Line(i), Def_File(name)) => Some((i, name))
         case (_, Def_File(name)) => Some((1, name))
         case _ => None
       }
   }
 
-  object Range
-  {
+  object Range {
     def apply(range: Symbol.Range): T = Offset(range.start) ::: End_Offset(range.stop)
     def unapply(pos: T): Option[Symbol.Range] =
       (pos, pos) match {
         case (Offset(start), End_Offset(stop)) if start <= stop => Some(Text.Range(start, stop))
         case (Offset(start), _) => Some(Text.Range(start, start + 1))
         case _ => None
       }
   }
 
-  object Def_Range
-  {
+  object Def_Range {
     def apply(range: Symbol.Range): T = Def_Offset(range.start) ::: Def_End_Offset(range.stop)
     def unapply(pos: T): Option[Symbol.Range] =
       (pos, pos) match {
         case (Def_Offset(start), Def_End_Offset(stop)) if start <= stop => Some(Text.Range(start, stop))
         case (Def_Offset(start), _) => Some(Text.Range(start, start + 1))
         case _ => None
       }
   }
 
-  object Item_Id
-  {
+  object Item_Id {
     def unapply(pos: T): Option[(Long, Symbol.Range)] =
       pos match {
         case Id(id) =>
           val offset = Offset.unapply(pos) getOrElse 0
           val end_offset = End_Offset.unapply(pos) getOrElse (offset + 1)
           Some((id, Text.Range(offset, end_offset)))
         case _ => None
       }
   }
 
-  object Item_Def_Id
-  {
+  object Item_Def_Id {
     def unapply(pos: T): Option[(Long, Symbol.Range)] =
       pos match {
         case Def_Id(id) =>
           val offset = Def_Offset.unapply(pos) getOrElse 0
           val end_offset = Def_End_Offset.unapply(pos) getOrElse (offset + 1)
           Some((id, Text.Range(offset, end_offset)))
         case _ => None
       }
   }
 
-  object Item_File
-  {
+  object Item_File {
     def unapply(pos: T): Option[(String, Int, Symbol.Range)] =
       pos match {
         case Line_File(line, name) =>
           val offset = Offset.unapply(pos) getOrElse 0
           val end_offset = End_Offset.unapply(pos) getOrElse (offset + 1)
           Some((name, line, Text.Range(offset, end_offset)))
         case _ => None
       }
   }
 
-  object Item_Def_File
-  {
+  object Item_Def_File {
     def unapply(pos: T): Option[(String, Int, Symbol.Range)] =
       pos match {
         case Def_Line_File(line, name) =>
           val offset = Def_Offset.unapply(pos) getOrElse 0
           val end_offset = Def_End_Offset.unapply(pos) getOrElse (offset + 1)

   }
 
 
   /* here: user output */
 
-  def here(props: T, delimited: Boolean = true): String =
-  {
+  def here(props: T, delimited: Boolean = true): String = {
     val pos = props.filter(Markup.position_property)
     if (pos.isEmpty) ""
     else {
       val s0 =
         (Line.unapply(pos), File.unapply(pos)) match {

   }
 
 
   /* JSON representation */
 
-  object JSON
-  {
+  object JSON {
     def apply(pos: T): isabelle.JSON.Object.T =
       isabelle.JSON.Object.empty ++
         Line.unapply(pos).map(Line.name -> _) ++
         Offset.unapply(pos).map(Offset.name -> _) ++
         End_Offset.unapply(pos).map(End_Offset.name -> _) ++