more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
authorwenzelm
Sat Aug 14 22:45:23 2010 +0200 (2010-08-14)
changeset 3841449f1f657adc2
parent 38413 224efb14f258
child 38415 f3220ef79d51
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
added convenient Markup.Int/Long objects (Scala);
simplified "assign" message format -- explicit version id;
misc tuning and simplification;
src/Pure/General/markup.ML
src/Pure/General/markup.scala
src/Pure/General/pretty.scala
src/Pure/PIDE/document.ML
src/Pure/PIDE/document.scala
src/Pure/System/isar_document.ML
src/Pure/System/isar_document.scala
src/Pure/System/session.scala
src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
     1.1 --- a/src/Pure/General/markup.ML	Sat Aug 14 21:25:20 2010 +0200
     1.2 +++ b/src/Pure/General/markup.ML	Sat Aug 14 22:45:23 2010 +0200
     1.3 @@ -6,6 +6,8 @@
     1.4  
     1.5  signature MARKUP =
     1.6  sig
     1.7 +  val parse_int: string -> int
     1.8 +  val print_int: int -> string
     1.9    type T = string * Properties.T
    1.10    val none: T
    1.11    val is_none: T -> bool
    1.12 @@ -109,8 +111,10 @@
    1.13    val failedN: string val failed: T
    1.14    val finishedN: string val finished: T
    1.15    val disposedN: string val disposed: T
    1.16 -  val assignN: string val assign: T
    1.17 -  val editN: string val edit: string -> string -> T
    1.18 +  val versionN: string
    1.19 +  val execN: string
    1.20 +  val assignN: string val assign: int -> T
    1.21 +  val editN: string val edit: int -> int -> T
    1.22    val pidN: string
    1.23    val promptN: string val prompt: T
    1.24    val readyN: string val ready: T
    1.25 @@ -127,6 +131,16 @@
    1.26  
    1.27  (** markup elements **)
    1.28  
    1.29 +(* integers *)
    1.30 +
    1.31 +fun parse_int s =
    1.32 +  (case Int.fromString s of
    1.33 +    SOME i => i
    1.34 +  | NONE => raise Fail ("Bad integer: " ^ quote s));
    1.35 +
    1.36 +val print_int = signed_string_of_int;
    1.37 +
    1.38 +
    1.39  (* basic markup *)
    1.40  
    1.41  type T = string * Properties.T;
    1.42 @@ -142,7 +156,7 @@
    1.43  
    1.44  fun markup_elem elem = (elem, (elem, []): T);
    1.45  fun markup_string elem prop = (elem, fn s => (elem, [(prop, s)]): T);
    1.46 -fun markup_int elem prop = (elem, fn i => (elem, [(prop, Int.toString i)]): T);
    1.47 +fun markup_int elem prop = (elem, fn i => (elem, [(prop, print_int i)]): T);
    1.48  
    1.49  
    1.50  (* name *)
    1.51 @@ -315,10 +329,12 @@
    1.52  
    1.53  (* interactive documents *)
    1.54  
    1.55 -val (assignN, assign) = markup_elem "assign";
    1.56 +val versionN = "version";
    1.57 +val execN = "exec";
    1.58 +val (assignN, assign) = markup_int "assign" versionN;
    1.59  
    1.60  val editN = "edit";
    1.61 -fun edit id state_id : T = (editN, [(idN, id), (stateN, state_id)]);
    1.62 +fun edit cmd_id exec_id : T = (editN, [(idN, print_int cmd_id), (execN, print_int exec_id)]);
    1.63  
    1.64  
    1.65  (* messages *)
     2.1 --- a/src/Pure/General/markup.scala	Sat Aug 14 21:25:20 2010 +0200
     2.2 +++ b/src/Pure/General/markup.scala	Sat Aug 14 22:45:23 2010 +0200
     2.3 @@ -9,34 +9,41 @@
     2.4  
     2.5  object Markup
     2.6  {
     2.7 +  /* integers */
     2.8 +
     2.9 +  object Int {
    2.10 +    def apply(i: scala.Int): String = i.toString
    2.11 +    def unapply(s: String): Option[scala.Int] =
    2.12 +      try { Some(Integer.parseInt(s)) }
    2.13 +      catch { case _: NumberFormatException => None }
    2.14 +  }
    2.15 +
    2.16 +  object Long {
    2.17 +    def apply(i: scala.Long): String = i.toString
    2.18 +    def unapply(s: String): Option[scala.Long] =
    2.19 +      try { Some(java.lang.Long.parseLong(s)) }
    2.20 +      catch { case _: NumberFormatException => None }
    2.21 +  }
    2.22 +
    2.23 +
    2.24    /* property values */
    2.25  
    2.26    def get_string(name: String, props: List[(String, String)]): Option[String] =
    2.27      props.find(p => p._1 == name).map(_._2)
    2.28  
    2.29 -
    2.30 -  def parse_long(s: String): Option[Long] =
    2.31 -    try { Some(java.lang.Long.parseLong(s)) }
    2.32 -    catch { case _: NumberFormatException => None }
    2.33 -
    2.34 -  def get_long(name: String, props: List[(String, String)]): Option[Long] =
    2.35 +  def get_long(name: String, props: List[(String, String)]): Option[scala.Long] =
    2.36    {
    2.37      get_string(name, props) match {
    2.38        case None => None
    2.39 -      case Some(value) => parse_long(value)
    2.40 +      case Some(Long(i)) => Some(i)
    2.41      }
    2.42    }
    2.43  
    2.44 -
    2.45 -  def parse_int(s: String): Option[Int] =
    2.46 -    try { Some(Integer.parseInt(s)) }
    2.47 -    catch { case _: NumberFormatException => None }
    2.48 -
    2.49 -  def get_int(name: String, props: List[(String, String)]): Option[Int] =
    2.50 +  def get_int(name: String, props: List[(String, String)]): Option[scala.Int] =
    2.51    {
    2.52      get_string(name, props) match {
    2.53        case None => None
    2.54 -      case Some(value) => parse_int(value)
    2.55 +      case Some(Int(i)) => Some(i)
    2.56      }
    2.57    }
    2.58  
    2.59 @@ -197,7 +204,9 @@
    2.60  
    2.61    /* interactive documents */
    2.62  
    2.63 -  val Assign = Markup("assign", Nil)
    2.64 +  val VERSION = "version"
    2.65 +  val EXEC = "exec"
    2.66 +  val ASSIGN = "assign"
    2.67    val EDIT = "edit"
    2.68  
    2.69  
     3.1 --- a/src/Pure/General/pretty.scala	Sat Aug 14 21:25:20 2010 +0200
     3.2 +++ b/src/Pure/General/pretty.scala	Sat Aug 14 22:45:23 2010 +0200
     3.3 @@ -16,29 +16,26 @@
     3.4  
     3.5    object Block
     3.6    {
     3.7 -    def apply(indent: Int, body: List[XML.Tree]): XML.Tree =
     3.8 -      XML.Elem(Markup(Markup.BLOCK, List((Markup.INDENT, indent.toString))), body)
     3.9 +    def apply(i: Int, body: List[XML.Tree]): XML.Tree =
    3.10 +      XML.Elem(Markup(Markup.BLOCK, List((Markup.INDENT, Markup.Int(i)))), body)
    3.11  
    3.12      def unapply(tree: XML.Tree): Option[(Int, List[XML.Tree])] =
    3.13        tree match {
    3.14 -        case XML.Elem(Markup(Markup.BLOCK, List((Markup.INDENT, indent))), body) =>
    3.15 -          Markup.parse_int(indent) match {
    3.16 -            case Some(i) => Some((i, body))
    3.17 -            case None => None
    3.18 -          }
    3.19 +        case XML.Elem(
    3.20 +          Markup(Markup.BLOCK, List((Markup.INDENT, Markup.Int(i)))), body) => Some((i, body))
    3.21          case _ => None
    3.22        }
    3.23    }
    3.24  
    3.25    object Break
    3.26    {
    3.27 -    def apply(width: Int): XML.Tree =
    3.28 -      XML.Elem(Markup(Markup.BREAK, List((Markup.WIDTH, width.toString))),
    3.29 -        List(XML.Text(Symbol.spaces(width))))
    3.30 +    def apply(w: Int): XML.Tree =
    3.31 +      XML.Elem(
    3.32 +        Markup(Markup.BREAK, List((Markup.WIDTH, Markup.Int(w)))), List(XML.Text(Symbol.spaces(w))))
    3.33  
    3.34      def unapply(tree: XML.Tree): Option[Int] =
    3.35        tree match {
    3.36 -        case XML.Elem(Markup(Markup.BREAK, List((Markup.WIDTH, width))), _) => Markup.parse_int(width)
    3.37 +        case XML.Elem(Markup(Markup.BREAK, List((Markup.WIDTH, Markup.Int(w)))), _) => Some(w)
    3.38          case _ => None
    3.39        }
    3.40    }
     4.1 --- a/src/Pure/PIDE/document.ML	Sat Aug 14 21:25:20 2010 +0200
     4.2 +++ b/src/Pure/PIDE/document.ML	Sat Aug 14 22:45:23 2010 +0200
     4.3 @@ -29,12 +29,8 @@
     4.4  
     4.5  val no_id = 0;
     4.6  
     4.7 -fun parse_id s =
     4.8 -  (case Int.fromString s of
     4.9 -    SOME i => i
    4.10 -  | NONE => raise Fail ("Bad id: " ^ quote s));
    4.11 -
    4.12 -val print_id = signed_string_of_int;
    4.13 +val parse_id = Markup.parse_int;
    4.14 +val print_id = Markup.print_int;
    4.15  
    4.16  
    4.17  (* edits *)
     5.1 --- a/src/Pure/PIDE/document.scala	Sat Aug 14 21:25:20 2010 +0200
     5.2 +++ b/src/Pure/PIDE/document.scala	Sat Aug 14 22:45:23 2010 +0200
     5.3 @@ -16,15 +16,18 @@
     5.4    /* formal identifiers */
     5.5  
     5.6    type ID = Long
     5.7 +
     5.8 +  object ID {
     5.9 +    def apply(id: ID): String = Markup.Long.apply(id)
    5.10 +    def unapply(s: String): Option[ID] = Markup.Long.unapply(s)
    5.11 +  }
    5.12 +
    5.13    type Version_ID = ID
    5.14    type Command_ID = ID
    5.15    type Exec_ID = ID
    5.16  
    5.17    val NO_ID: ID = 0
    5.18  
    5.19 -  def parse_id(s: String): ID = java.lang.Long.parseLong(s)
    5.20 -  def print_id(id: ID): String = id.toString
    5.21 -
    5.22  
    5.23  
    5.24    /** named document nodes **/
     6.1 --- a/src/Pure/System/isar_document.ML	Sat Aug 14 21:25:20 2010 +0200
     6.2 +++ b/src/Pure/System/isar_document.ML	Sat Aug 14 22:45:23 2010 +0200
     6.3 @@ -240,11 +240,9 @@
     6.4    in (exec_id', (id, exec_id') :: updates) end;
     6.5  
     6.6  fun updates_status new_id updates =
     6.7 -  implode (map (fn (id, exec_id) =>
     6.8 -      Markup.markup (Markup.edit (Document.print_id id) (Document.print_id exec_id)) "") updates)
     6.9 -  |> Markup.markup Markup.assign
    6.10 -  |> Position.setmp_thread_data (Position.id_only (Document.print_id new_id)) Output.status;
    6.11 -  (*FIXME avoid setmp -- direct message argument*)
    6.12 +  implode (map (fn (id, exec_id) => Markup.markup (Markup.edit id exec_id) "") updates)
    6.13 +  |> Markup.markup (Markup.assign new_id)
    6.14 +  |> Output.status;
    6.15  
    6.16  in
    6.17  
     7.1 --- a/src/Pure/System/isar_document.scala	Sat Aug 14 21:25:20 2010 +0200
     7.2 +++ b/src/Pure/System/isar_document.scala	Sat Aug 14 22:45:23 2010 +0200
     7.3 @@ -12,11 +12,12 @@
     7.4    /* protocol messages */
     7.5  
     7.6    object Assign {
     7.7 -    def unapply(msg: XML.Tree): Option[List[(Document.Command_ID, Document.Exec_ID)]] =
     7.8 +    def unapply(msg: XML.Tree)
     7.9 +        : Option[(Document.Version_ID, List[(Document.Command_ID, Document.Exec_ID)])] =
    7.10        msg match {
    7.11 -        case XML.Elem(Markup.Assign, edits) =>
    7.12 +        case XML.Elem(Markup(Markup.ASSIGN, List((Markup.VERSION, Document.ID(id)))), edits) =>
    7.13            val id_edits = edits.map(Edit.unapply)
    7.14 -          if (id_edits.forall(_.isDefined)) Some(id_edits.map(_.get))
    7.15 +          if (id_edits.forall(_.isDefined)) Some((id, id_edits.map(_.get)))
    7.16            else None
    7.17          case _ => None
    7.18        }
    7.19 @@ -25,11 +26,9 @@
    7.20    object Edit {
    7.21      def unapply(msg: XML.Tree): Option[(Document.Command_ID, Document.Exec_ID)] =
    7.22        msg match {
    7.23 -        case XML.Elem(Markup(Markup.EDIT, List((Markup.ID, cmd_id), (Markup.STATE, state_id))), Nil) =>
    7.24 -          (Markup.parse_long(cmd_id), Markup.parse_long(state_id)) match {
    7.25 -            case (Some(i), Some(j)) => Some((i, j))
    7.26 -            case _ => None
    7.27 -          }
    7.28 +        case XML.Elem(
    7.29 +          Markup(Markup.EDIT,
    7.30 +            List((Markup.ID, Document.ID(i)), (Markup.EXEC, Document.ID(j)))), Nil) => Some((i, j))
    7.31          case _ => None
    7.32        }
    7.33    }
    7.34 @@ -44,7 +43,7 @@
    7.35    /* commands */
    7.36  
    7.37    def define_command(id: Document.Command_ID, text: String): Unit =
    7.38 -    input("Isar_Document.define_command", Document.print_id(id), text)
    7.39 +    input("Isar_Document.define_command", Document.ID(id), text)
    7.40  
    7.41  
    7.42    /* documents */
    7.43 @@ -62,6 +61,6 @@
    7.44                XML_Data.make_pair(make_id1)(XML_Data.make_option(XML_Data.make_long))))))(edits)
    7.45  
    7.46      input("Isar_Document.edit_document",
    7.47 -      Document.print_id(old_id), Document.print_id(new_id), YXML.string_of_body(arg))
    7.48 +      Document.ID(old_id), Document.ID(new_id), YXML.string_of_body(arg))
    7.49    }
    7.50  }
     8.1 --- a/src/Pure/System/session.scala	Sat Aug 14 21:25:20 2010 +0200
     8.2 +++ b/src/Pure/System/session.scala	Sat Aug 14 22:45:23 2010 +0200
     8.3 @@ -132,27 +132,19 @@
     8.4        raw_results.event(result)
     8.5  
     8.6        Position.get_id(result.properties) match {
     8.7 -        case Some(target_id) =>
     8.8 +        case Some(state_id) =>
     8.9            try {
    8.10 -            val (st, state) = global_state.accumulate(target_id, result.message)
    8.11 +            val (st, state) = global_state.accumulate(state_id, result.message)
    8.12              global_state = state
    8.13 -            indicate_command_change(st.command)  // FIXME forward Command.State (!?)
    8.14 +            indicate_command_change(st.command)
    8.15            }
    8.16 -          catch {
    8.17 -            case _: Document.State.Fail =>
    8.18 -              if (result.is_status) {
    8.19 -                result.body match {
    8.20 -                  case List(Isar_Document.Assign(edits)) =>
    8.21 -                    try { change_state(_.assign(target_id, edits)) }
    8.22 -                    catch { case _: Document.State.Fail => bad_result(result) }
    8.23 -                  case _ => bad_result(result)
    8.24 -                }
    8.25 -              }
    8.26 -              else bad_result(result)
    8.27 -          }
    8.28 +          catch { case _: Document.State.Fail => bad_result(result) }
    8.29          case None =>
    8.30            if (result.is_status) {
    8.31              result.body match {
    8.32 +              case List(Isar_Document.Assign(doc_id, edits)) =>
    8.33 +                try { change_state(_.assign(doc_id, edits)) }
    8.34 +                catch { case _: Document.State.Fail => bad_result(result) }
    8.35                case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
    8.36                case List(Keyword.Keyword_Decl(name)) => syntax += name
    8.37                case _ => if (!result.is_ready) bad_result(result)
     9.1 --- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Sat Aug 14 21:25:20 2010 +0200
     9.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Sat Aug 14 22:45:23 2010 +0200
     9.3 @@ -139,7 +139,7 @@
     9.4                override def getIcon: Icon = null
     9.5                override def getShortString: String = content
     9.6                override def getLongString: String = node.info.toString
     9.7 -              override def getName: String = Document.print_id(id)
     9.8 +              override def getName: String = Markup.Long(id)
     9.9                override def setName(name: String) = ()
    9.10                override def setStart(start: Position) = ()
    9.11                override def getStart: Position = command_start + node.start