# HG changeset patch # User wenzelm # Date 1347967125 -7200 # Node ID d7b5fb2e9ca20d2816cd340fb3331c17fac30080 # Parent 8c9925d31617c7f81bd49a824a42daa6da31d905 some support for inital command markup; tuned signature; diff -r 8c9925d31617 -r d7b5fb2e9ca2 src/Pure/General/pretty.scala --- a/src/Pure/General/pretty.scala Tue Sep 18 11:49:23 2012 +0200 +++ b/src/Pure/General/pretty.scala Tue Sep 18 13:18:45 2012 +0200 @@ -146,7 +146,7 @@ def string_of(input: XML.Body, margin: Int = margin_default, metric: String => Double = metric_default): String = - formatted(input, margin, metric).iterator.flatMap(XML.content).mkString + XML.content(formatted(input, margin, metric)).mkString /* unformatted output */ @@ -164,6 +164,5 @@ input.flatMap(standard_format).flatMap(fmt) } - def str_of(input: XML.Body): String = - unformatted(input).iterator.flatMap(XML.content).mkString + def str_of(input: XML.Body): String = XML.content(unformatted(input)).mkString } diff -r 8c9925d31617 -r d7b5fb2e9ca2 src/Pure/PIDE/blob.scala --- a/src/Pure/PIDE/blob.scala Tue Sep 18 11:49:23 2012 +0200 +++ b/src/Pure/PIDE/blob.scala Tue Sep 18 13:18:45 2012 +0200 @@ -24,5 +24,5 @@ def decode(i: Text.Offset): Text.Offset = symbol_index.decode(i) def decode(r: Text.Range): Text.Range = symbol_index.decode(r) - val empty_state: Blob.State = Blob.State(this) + val init_state: Blob.State = Blob.State(this) } diff -r 8c9925d31617 -r d7b5fb2e9ca2 src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Tue Sep 18 11:49:23 2012 +0200 +++ b/src/Pure/PIDE/command.scala Tue Sep 18 13:18:45 2012 +0200 @@ -79,7 +79,8 @@ type Span = List[Token] - def apply(id: Document.Command_ID, node_name: Document.Node.Name, span: Span): Command = + def apply(id: Document.Command_ID, node_name: Document.Node.Name, + span: Span, markup: Markup_Tree): Command = { val source: String = span match { @@ -96,13 +97,22 @@ i += n } - new Command(id, node_name, span1.toList, source) + new Command(id, node_name, span1.toList, source, markup) } - def unparsed(source: String): Command = - Command(Document.no_id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source))) + val empty = Command(Document.no_id, Document.Node.Name.empty, Nil, Markup_Tree.empty) + + def unparsed(id: Document.Command_ID, source: String, markup: Markup_Tree): Command = + Command(id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source)), markup) + + def unparsed(source: String): Command = unparsed(Document.no_id, source, Markup_Tree.empty) - val empty = Command(Document.no_id, Document.Node.Name.empty, Nil) + def rich_text(id: Document.Command_ID, body: XML.Body): Command = + { + val text = XML.content(body).mkString + val markup = Markup_Tree.empty // FIXME + unparsed(id, text, markup) + } /* perspective */ @@ -131,7 +141,8 @@ val id: Document.Command_ID, val node_name: Document.Node.Name, val span: Command.Span, - val source: String) + val source: String, + val init_markup: Markup_Tree) { /* classification */ @@ -167,5 +178,5 @@ /* accumulated results */ - val empty_state: Command.State = Command.State(this) + val init_state: Command.State = Command.State(this, markup = init_markup) } diff -r 8c9925d31617 -r d7b5fb2e9ca2 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Tue Sep 18 11:49:23 2012 +0200 +++ b/src/Pure/PIDE/document.scala Tue Sep 18 13:18:45 2012 +0200 @@ -350,7 +350,7 @@ def define_command(command: Command): State = { val id = command.id - copy(commands = commands + (id -> command.empty_state)) + copy(commands = commands + (id -> command.init_state)) } def defined_command(id: Command_ID): Boolean = commands.isDefinedAt(id) @@ -474,7 +474,7 @@ catch { case _: State.Fail => try { the_command_state(command.id) } - catch { case _: State.Fail => command.empty_state } + catch { case _: State.Fail => command.init_state } } } diff -r 8c9925d31617 -r d7b5fb2e9ca2 src/Pure/Thy/thy_syntax.scala --- a/src/Pure/Thy/thy_syntax.scala Tue Sep 18 11:49:23 2012 +0200 +++ b/src/Pure/Thy/thy_syntax.scala Tue Sep 18 13:18:45 2012 +0200 @@ -68,7 +68,7 @@ /* result structure */ val spans = parse_spans(syntax.scan(text)) - spans.foreach(span => add(Command(Document.no_id, node_name, span))) + spans.foreach(span => add(Command(Document.no_id, node_name, span, Markup_Tree.empty))) result() } } @@ -226,7 +226,7 @@ commands case cmd :: _ => val hook = commands.prev(cmd) - val inserted = spans2.map(span => Command(Document.new_id(), name, span)) + val inserted = spans2.map(span => Command(Document.new_id(), name, span, Markup_Tree.empty)) (commands /: cmds2)(_ - _).append_after(hook, inserted) } } diff -r 8c9925d31617 -r d7b5fb2e9ca2 src/Tools/jEdit/src/output2_dockable.scala --- a/src/Tools/jEdit/src/output2_dockable.scala Tue Sep 18 11:49:23 2012 +0200 +++ b/src/Tools/jEdit/src/output2_dockable.scala Tue Sep 18 13:18:45 2012 +0200 @@ -31,7 +31,7 @@ private var zoom_factor = 100 private var show_tracing = false private var do_update = true - private var current_state = Command.empty.empty_state + private var current_state = Command.empty.init_state private var current_body: XML.Body = Nil @@ -60,9 +60,9 @@ val snapshot = doc_view.model.snapshot() snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match { case Some(cmd) => snapshot.state.command_state(snapshot.version, cmd) - case None => Command.empty.empty_state + case None => Command.empty.init_state } - case None => Command.empty.empty_state + case None => Command.empty.init_state } } else current_state diff -r 8c9925d31617 -r d7b5fb2e9ca2 src/Tools/jEdit/src/output_dockable.scala --- a/src/Tools/jEdit/src/output_dockable.scala Tue Sep 18 11:49:23 2012 +0200 +++ b/src/Tools/jEdit/src/output_dockable.scala Tue Sep 18 13:18:45 2012 +0200 @@ -31,7 +31,7 @@ private var zoom_factor = 100 private var show_tracing = false private var do_update = true - private var current_state = Command.empty.empty_state + private var current_state = Command.empty.init_state private var current_body: XML.Body = Nil @@ -91,9 +91,9 @@ val snapshot = doc_view.model.snapshot() snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match { case Some(cmd) => snapshot.state.command_state(snapshot.version, cmd) - case None => Command.empty.empty_state + case None => Command.empty.init_state } - case None => Command.empty.empty_state + case None => Command.empty.init_state } } else current_state diff -r 8c9925d31617 -r d7b5fb2e9ca2 src/Tools/jEdit/src/pretty_text_area.scala --- a/src/Tools/jEdit/src/pretty_text_area.scala Tue Sep 18 11:49:23 2012 +0200 +++ b/src/Tools/jEdit/src/pretty_text_area.scala Tue Sep 18 13:18:45 2012 +0200 @@ -22,15 +22,11 @@ { def document_state(formatted_body: XML.Body): Document.State = { - val text = formatted_body.iterator.flatMap(XML.content).mkString - val markup: List[XML.Elem] = Nil // FIXME - - val command = Command.unparsed(text) + val command = Command.rich_text(Document.new_id(), formatted_body) val node_name = command.node_name - val exec_id = Document.new_id() val edits: List[Document.Edit_Text] = - List(node_name -> Document.Node.Edits(List(Text.Edit.insert(0, text)))) + List(node_name -> Document.Node.Edits(List(Text.Edit.insert(0, command.source)))) val state0 = Document.State.init.define_command(command) val version0 = state0.history.tip.version.get_finished @@ -41,7 +37,7 @@ val state1 = state0.continue_history(Future.value(version0), edits, Future.value(version1))._2 .define_version(version1, state0.the_assignment(version0)) - .assign(version1.id, List(command.id -> Some(exec_id)))._2 + .assign(version1.id, List(command.id -> Some(Document.new_id())))._2 state1 }