src/Pure/PIDE/command.scala
author wenzelm
Tue, 29 Nov 2011 21:50:00 +0100
changeset 45674 eb65c9d17e2f
parent 45672 a497c5d4a523
child 45709 87017fcbad83
permissions -rw-r--r--
clarified Time vs. Timing;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
36676
ac7961d42ac3 some rearrangement of Scala sources;
wenzelm
parents: 36012
diff changeset
     1
/*  Title:      Pure/PIDE/command.scala
ac7961d42ac3 some rearrangement of Scala sources;
wenzelm
parents: 36012
diff changeset
     2
    Author:     Fabian Immler, TU Munich
ac7961d42ac3 some rearrangement of Scala sources;
wenzelm
parents: 36012
diff changeset
     3
    Author:     Makarius
ac7961d42ac3 some rearrangement of Scala sources;
wenzelm
parents: 36012
diff changeset
     4
ac7961d42ac3 some rearrangement of Scala sources;
wenzelm
parents: 36012
diff changeset
     5
Prover commands with semantic state.
ac7961d42ac3 some rearrangement of Scala sources;
wenzelm
parents: 36012
diff changeset
     6
*/
34407
aad6834ba380 added some headers and comments;
wenzelm
parents: 34401
diff changeset
     7
34871
e596a0b71f3c incorporate "proofdocument" part into main Isabelle/Pure.jar -- except for html_panel.scala, which depends on external library (Lobo/Cobra browser);
wenzelm
parents: 34865
diff changeset
     8
package isabelle
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
     9
43520
cec9b95fa35d explicit import java.lang.System to prevent odd scope problems;
wenzelm
parents: 40572
diff changeset
    10
import java.lang.System
34451
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
    11
45644
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
    12
import scala.collection.mutable
38872
26c505765024 Command.results: ordered by serial number;
wenzelm
parents: 38723
diff changeset
    13
import scala.collection.immutable.SortedMap
26c505765024 Command.results: ordered by serial number;
wenzelm
parents: 38723
diff changeset
    14
26c505765024 Command.results: ordered by serial number;
wenzelm
parents: 38723
diff changeset
    15
34637
f3b5d6e248be added symbol_index (presently unused);
wenzelm
parents: 34603
diff changeset
    16
object Command
f3b5d6e248be added symbol_index (presently unused);
wenzelm
parents: 34603
diff changeset
    17
{
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    18
  /** accumulated results from prover **/
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    19
43714
3749d1e6dde9 tuned signature;
wenzelm
parents: 43662
diff changeset
    20
  sealed case class State(
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    21
    val command: Command,
38872
26c505765024 Command.results: ordered by serial number;
wenzelm
parents: 38723
diff changeset
    22
    val status: List[Markup] = Nil,
26c505765024 Command.results: ordered by serial number;
wenzelm
parents: 38723
diff changeset
    23
    val results: SortedMap[Long, XML.Tree] = SortedMap.empty,
26c505765024 Command.results: ordered by serial number;
wenzelm
parents: 38723
diff changeset
    24
    val markup: Markup_Tree = Markup_Tree.empty)
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    25
  {
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    26
    /* content */
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    27
38714
31da698fc4e5 more precise Command.State accumulation;
wenzelm
parents: 38658
diff changeset
    28
    def add_status(st: Markup): State = copy(status = st :: status)
45455
4f974c0c5c2f prefer statically typed Text.Markup;
wenzelm
parents: 44959
diff changeset
    29
    def add_markup(m: Text.Markup): State = copy(markup = markup + m)
38872
26c505765024 Command.results: ordered by serial number;
wenzelm
parents: 38723
diff changeset
    30
    def add_result(serial: Long, result: XML.Tree): State =
26c505765024 Command.results: ordered by serial number;
wenzelm
parents: 38723
diff changeset
    31
      copy(results = results + (serial -> result))
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    32
45455
4f974c0c5c2f prefer statically typed Text.Markup;
wenzelm
parents: 44959
diff changeset
    33
    def root_info: Text.Markup =
4f974c0c5c2f prefer statically typed Text.Markup;
wenzelm
parents: 44959
diff changeset
    34
      Text.Info(command.range,
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45644
diff changeset
    35
        XML.Elem(Markup(Isabelle_Markup.STATUS, Nil), status.reverse.map(XML.Elem(_, Nil))))
38658
20d82e98bcd7 tuned root markup;
wenzelm
parents: 38637
diff changeset
    36
    def root_markup: Markup_Tree = markup + root_info
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    37
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    38
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    39
    /* message dispatch */
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    40
38872
26c505765024 Command.results: ordered by serial number;
wenzelm
parents: 38723
diff changeset
    41
    def accumulate(message: XML.Elem): Command.State =
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    42
      message match {
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45644
diff changeset
    43
        case XML.Elem(Markup(Isabelle_Markup.STATUS, _), msgs) =>
38714
31da698fc4e5 more precise Command.State accumulation;
wenzelm
parents: 38658
diff changeset
    44
          (this /: msgs)((state, msg) =>
31da698fc4e5 more precise Command.State accumulation;
wenzelm
parents: 38658
diff changeset
    45
            msg match {
31da698fc4e5 more precise Command.State accumulation;
wenzelm
parents: 38658
diff changeset
    46
              case XML.Elem(markup, Nil) => state.add_status(markup)
31da698fc4e5 more precise Command.State accumulation;
wenzelm
parents: 38658
diff changeset
    47
              case _ => System.err.println("Ignored status message: " + msg); state
31da698fc4e5 more precise Command.State accumulation;
wenzelm
parents: 38658
diff changeset
    48
            })
38581
d503a0912e14 simplified Command.status again, reverting most of e5eed57913d0 (note that more complex information can be represented with full markup reports);
wenzelm
parents: 38579
diff changeset
    49
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45644
diff changeset
    50
        case XML.Elem(Markup(Isabelle_Markup.REPORT, _), msgs) =>
38572
0fe2c01ef7da Command.State: accumulate markup reports uniformly;
wenzelm
parents: 38564
diff changeset
    51
          (this /: msgs)((state, msg) =>
0fe2c01ef7da Command.State: accumulate markup reports uniformly;
wenzelm
parents: 38564
diff changeset
    52
            msg match {
39173
ed3946086358 Command.State.accumulate: check actual source range;
wenzelm
parents: 39172
diff changeset
    53
              case XML.Elem(Markup(name, atts @ Position.Id_Range(id, raw_range)), args)
ed3946086358 Command.State.accumulate: check actual source range;
wenzelm
parents: 39172
diff changeset
    54
              if id == command.id && command.range.contains(command.decode(raw_range)) =>
ed3946086358 Command.State.accumulate: check actual source range;
wenzelm
parents: 39172
diff changeset
    55
                val range = command.decode(raw_range)
38872
26c505765024 Command.results: ordered by serial number;
wenzelm
parents: 38723
diff changeset
    56
                val props = Position.purge(atts)
45455
4f974c0c5c2f prefer statically typed Text.Markup;
wenzelm
parents: 44959
diff changeset
    57
                val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
38723
wenzelm
parents: 38722
diff changeset
    58
                state.add_markup(info)
40572
2315c3daee74 avoid spam;
wenzelm
parents: 40454
diff changeset
    59
              case _ =>
2315c3daee74 avoid spam;
wenzelm
parents: 40454
diff changeset
    60
                // FIXME System.err.println("Ignored report message: " + msg)
2315c3daee74 avoid spam;
wenzelm
parents: 40454
diff changeset
    61
                state
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    62
            })
38872
26c505765024 Command.results: ordered by serial number;
wenzelm
parents: 38723
diff changeset
    63
        case XML.Elem(Markup(name, atts), body) =>
26c505765024 Command.results: ordered by serial number;
wenzelm
parents: 38723
diff changeset
    64
          atts match {
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45644
diff changeset
    65
            case Isabelle_Markup.Serial(i) =>
38887
1261481ef5e5 Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents: 38877
diff changeset
    66
              val result = XML.Elem(Markup(name, Position.purge(atts)), body)
39622
53365ba766ac Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;
wenzelm
parents: 39441
diff changeset
    67
              val st0 = add_result(i, result)
39441
4110cc1b8f9f allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents: 39173
diff changeset
    68
              val st1 =
45672
a497c5d4a523 clarified modules;
wenzelm
parents: 45666
diff changeset
    69
                if (Isabelle_Document.is_tracing(message)) st0
39622
53365ba766ac Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;
wenzelm
parents: 39441
diff changeset
    70
                else
45672
a497c5d4a523 clarified modules;
wenzelm
parents: 45666
diff changeset
    71
                  (st0 /: Isabelle_Document.message_positions(command, message))(
39622
53365ba766ac Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;
wenzelm
parents: 39441
diff changeset
    72
                    (st, range) => st.add_markup(Text.Info(range, result)))
45672
a497c5d4a523 clarified modules;
wenzelm
parents: 45666
diff changeset
    73
              val st2 = (st1 /: Isabelle_Document.message_reports(message))(_ accumulate _)
39622
53365ba766ac Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;
wenzelm
parents: 39441
diff changeset
    74
              st2
38872
26c505765024 Command.results: ordered by serial number;
wenzelm
parents: 38723
diff changeset
    75
            case _ => System.err.println("Ignored message without serial number: " + message); this
26c505765024 Command.results: ordered by serial number;
wenzelm
parents: 38723
diff changeset
    76
          }
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    77
      }
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
    78
  }
38367
f7d2574dc3a6 more basic notion of unparsed input;
wenzelm
parents: 38363
diff changeset
    79
f7d2574dc3a6 more basic notion of unparsed input;
wenzelm
parents: 38363
diff changeset
    80
45644
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
    81
  /* make commands */
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
    82
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
    83
  def apply(id: Document.Command_ID, node_name: Document.Node.Name, toks: List[Token]): Command =
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
    84
  {
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
    85
    val source: String =
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
    86
      toks match {
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
    87
        case List(tok) => tok.source
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
    88
        case _ => toks.map(_.source).mkString
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
    89
      }
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
    90
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
    91
    val span = new mutable.ListBuffer[Token]
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
    92
    var i = 0
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
    93
    for (Token(kind, s) <- toks) {
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
    94
      val n = s.length
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
    95
      val s1 = source.substring(i, i + n)
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
    96
      span += Token(kind, s1)
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
    97
      i += n
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
    98
    }
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
    99
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
   100
    new Command(id, node_name, span.toList, source)
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
   101
  }
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
   102
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
   103
  def apply(node_name: Document.Node.Name, toks: List[Token]): Command =
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
   104
    Command(Document.no_id, node_name, toks)
38367
f7d2574dc3a6 more basic notion of unparsed input;
wenzelm
parents: 38363
diff changeset
   105
40454
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 39622
diff changeset
   106
  def unparsed(source: String): Command =
45644
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
   107
    Command(Document.no_id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source)))
44384
8f6054a63f96 some support for editor perspective;
wenzelm
parents: 43714
diff changeset
   108
8f6054a63f96 some support for editor perspective;
wenzelm
parents: 43714
diff changeset
   109
8f6054a63f96 some support for editor perspective;
wenzelm
parents: 43714
diff changeset
   110
  /* perspective */
8f6054a63f96 some support for editor perspective;
wenzelm
parents: 43714
diff changeset
   111
44474
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   112
  object Perspective
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   113
  {
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   114
    val empty: Perspective = Perspective(Nil)
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   115
  }
44385
e7fdb008aa7d propagate editor perspective through document model;
wenzelm
parents: 44384
diff changeset
   116
44474
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   117
  sealed case class Perspective(commands: List[Command])  // visible commands in canonical order
44385
e7fdb008aa7d propagate editor perspective through document model;
wenzelm
parents: 44384
diff changeset
   118
  {
44474
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   119
    def same(that: Perspective): Boolean =
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   120
    {
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   121
      val cmds1 = this.commands
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   122
      val cmds2 = that.commands
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   123
      require(cmds1.forall(_.is_defined))
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   124
      require(cmds2.forall(_.is_defined))
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   125
      cmds1.length == cmds2.length &&
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   126
        (cmds1.iterator zip cmds2.iterator).forall({ case (c1, c2) => c1.id == c2.id })
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44385
diff changeset
   127
    }
44385
e7fdb008aa7d propagate editor perspective through document model;
wenzelm
parents: 44384
diff changeset
   128
  }
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   129
}
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   130
38361
b609d0b271fa specific command state;
wenzelm
parents: 38360
diff changeset
   131
45644
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
   132
class Command private(
38150
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents: 37373
diff changeset
   133
    val id: Document.Command_ID,
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44607
diff changeset
   134
    val node_name: Document.Node.Name,
45644
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
   135
    val span: List[Token],
8634b4e61b88 sharing of token source with span source;
wenzelm
parents: 45455
diff changeset
   136
    val source: String)
34451
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
   137
{
34859
f986d84dd44b renamed Command.content to source;
wenzelm
parents: 34858
diff changeset
   138
  /* classification */
34500
384427c750c8 state_results: separate buffer for messages from running command;
wenzelm
parents: 34497
diff changeset
   139
44385
e7fdb008aa7d propagate editor perspective through document model;
wenzelm
parents: 44384
diff changeset
   140
  def is_defined: Boolean = id != Document.no_id
e7fdb008aa7d propagate editor perspective through document model;
wenzelm
parents: 44384
diff changeset
   141
36012
0614676f14d4 replaced some deprecated methods;
wenzelm
parents: 34871
diff changeset
   142
  def is_command: Boolean = !span.isEmpty && span.head.is_command
34865
104298db6abf Outer_Lex.is_ignored;
wenzelm
parents: 34860
diff changeset
   143
  def is_ignored: Boolean = span.forall(_.is_ignored)
34859
f986d84dd44b renamed Command.content to source;
wenzelm
parents: 34858
diff changeset
   144
  def is_malformed: Boolean = !is_command && !is_ignored
f986d84dd44b renamed Command.content to source;
wenzelm
parents: 34858
diff changeset
   145
36012
0614676f14d4 replaced some deprecated methods;
wenzelm
parents: 34871
diff changeset
   146
  def name: String = if (is_command) span.head.content else ""
37129
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 36990
diff changeset
   147
  override def toString =
37373
25078ba44436 tuned Command.toString -- preserving uniqueness allows the Scala toplevel to print Linear_Set[Command] results without crashing;
wenzelm
parents: 37197
diff changeset
   148
    id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED")
34495
722533c532da Command: added name field and toString;
wenzelm
parents: 34491
diff changeset
   149
34859
f986d84dd44b renamed Command.content to source;
wenzelm
parents: 34858
diff changeset
   150
f986d84dd44b renamed Command.content to source;
wenzelm
parents: 34858
diff changeset
   151
  /* source text */
34451
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
   152
38426
2858ec7b6dd8 specific types Text.Offset and Text.Range;
wenzelm
parents: 38415
diff changeset
   153
  def source(range: Text.Range): String = source.substring(range.start, range.stop)
34859
f986d84dd44b renamed Command.content to source;
wenzelm
parents: 34858
diff changeset
   154
  def length: Int = source.length
38572
0fe2c01ef7da Command.State: accumulate markup reports uniformly;
wenzelm
parents: 38564
diff changeset
   155
38877
682c4932b3cc Command.newlines: account for physical newlines;
wenzelm
parents: 38872
diff changeset
   156
  val newlines =
682c4932b3cc Command.newlines: account for physical newlines;
wenzelm
parents: 38872
diff changeset
   157
    (0 /: Symbol.iterator(source)) {
682c4932b3cc Command.newlines: account for physical newlines;
wenzelm
parents: 38872
diff changeset
   158
      case (n, s) => if (Symbol.is_physical_newline(s)) n + 1 else n }
682c4932b3cc Command.newlines: account for physical newlines;
wenzelm
parents: 38872
diff changeset
   159
38479
e628da370072 more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents: 38476
diff changeset
   160
  val range: Text.Range = Text.Range(0, length)
34855
81d0410dc3ac iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents: 34835
diff changeset
   161
34859
f986d84dd44b renamed Command.content to source;
wenzelm
parents: 34858
diff changeset
   162
  lazy val symbol_index = new Symbol.Index(source)
38579
ce46a6f55bce tuned signature;
wenzelm
parents: 38577
diff changeset
   163
  def decode(i: Text.Offset): Text.Offset = symbol_index.decode(i)
ce46a6f55bce tuned signature;
wenzelm
parents: 38577
diff changeset
   164
  def decode(r: Text.Range): Text.Range = symbol_index.decode(r)
38370
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   165
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   166
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   167
  /* accumulated results */
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38367
diff changeset
   168
38872
26c505765024 Command.results: ordered by serial number;
wenzelm
parents: 38723
diff changeset
   169
  val empty_state: Command.State = Command.State(this)
34676
9e725d34df7b Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents: 34675
diff changeset
   170
}