merged
authorwenzelm
Fri Sep 02 23:04:12 2011 +0200 (2011-09-02 ago)
changeset 44665178a6f0ed29d
parent 44664 f64c715660c3
parent 44662 c8f1d943bfc5
child 44671 7f0b4515588a
merged
     1.1 --- a/src/Pure/General/markup.ML	Fri Sep 02 19:29:48 2011 +0200
     1.2 +++ b/src/Pure/General/markup.ML	Fri Sep 02 23:04:12 2011 +0200
     1.3 @@ -107,8 +107,6 @@
     1.4    val joinedN: string val joined: T
     1.5    val failedN: string val failed: T
     1.6    val finishedN: string val finished: T
     1.7 -  val versionN: string
     1.8 -  val assignN: string val assign: int -> T
     1.9    val serialN: string
    1.10    val legacyN: string val legacy: T
    1.11    val promptN: string val prompt: T
    1.12 @@ -117,6 +115,7 @@
    1.13    val no_reportN: string val no_report: T
    1.14    val badN: string val bad: T
    1.15    val functionN: string
    1.16 +  val assign_execs: Properties.T
    1.17    val invoke_scala: string -> string -> Properties.T
    1.18    val cancel_scala: string -> Properties.T
    1.19    val no_output: Output.output * Output.output
    1.20 @@ -349,12 +348,6 @@
    1.21  val (finishedN, finished) = markup_elem "finished";
    1.22  
    1.23  
    1.24 -(* interactive documents *)
    1.25 -
    1.26 -val versionN = "version";
    1.27 -val (assignN, assign) = markup_int "assign" versionN;
    1.28 -
    1.29 -
    1.30  (* messages *)
    1.31  
    1.32  val serialN = "serial";
    1.33 @@ -373,6 +366,8 @@
    1.34  
    1.35  val functionN = "function"
    1.36  
    1.37 +val assign_execs = [(functionN, "assign_execs")];
    1.38 +
    1.39  fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)];
    1.40  fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)];
    1.41  
     2.1 --- a/src/Pure/General/markup.scala	Fri Sep 02 19:29:48 2011 +0200
     2.2 +++ b/src/Pure/General/markup.scala	Fri Sep 02 23:04:12 2011 +0200
     2.3 @@ -273,6 +273,8 @@
     2.4    val FUNCTION = "function"
     2.5    val Function = new Properties.String(FUNCTION)
     2.6  
     2.7 +  val Assign_Execs: Properties.T = List((FUNCTION, "assign_execs"))
     2.8 +
     2.9    val INVOKE_SCALA = "invoke_scala"
    2.10    object Invoke_Scala
    2.11    {
     3.1 --- a/src/Pure/Isar/outer_syntax.ML	Fri Sep 02 19:29:48 2011 +0200
     3.2 +++ b/src/Pure/Isar/outer_syntax.ML	Fri Sep 02 23:04:12 2011 +0200
     3.3 @@ -34,10 +34,9 @@
     3.4    val process_file: Path.T -> theory -> theory
     3.5    type isar
     3.6    val isar: TextIO.instream -> bool -> isar
     3.7 -  val read_span: outer_syntax -> Thy_Syntax.span -> Toplevel.transition * bool
     3.8 +  val read_command: Position.T -> string -> Toplevel.transition
     3.9    val read_element: outer_syntax -> (unit -> theory) -> Thy_Syntax.element ->
    3.10      (Toplevel.transition * Toplevel.transition list) list
    3.11 -  val read_command: Position.T -> string -> Toplevel.transition
    3.12  end;
    3.13  
    3.14  structure Outer_Syntax: OUTER_SYNTAX =
    3.15 @@ -255,38 +254,37 @@
    3.16  
    3.17  val not_singleton = "Exactly one command expected";
    3.18  
    3.19 -fun read_span outer_syntax span =
    3.20 +fun read_span outer_syntax toks =
    3.21    let
    3.22      val commands = lookup_commands outer_syntax;
    3.23 -    val range_pos = Position.set_range (Thy_Syntax.span_range span);
    3.24 -    val toks = Thy_Syntax.span_content span;
    3.25 +    val range_pos = Position.set_range (Token.range toks);
    3.26      val _ = List.app Thy_Syntax.report_token toks;
    3.27    in
    3.28      (case Source.exhaust (toplevel_source false NONE (K commands) (Source.of_list toks)) of
    3.29        [tr] =>
    3.30          if Keyword.is_control (Toplevel.name_of tr) then
    3.31 -          (Toplevel.malformed range_pos "Illegal control command", true)
    3.32 +          (Toplevel.malformed (Toplevel.pos_of tr) "Illegal control command", true)
    3.33          else (tr, true)
    3.34      | [] => (Toplevel.ignored range_pos, false)
    3.35      | _ => (Toplevel.malformed range_pos not_singleton, true))
    3.36      handle ERROR msg => (Toplevel.malformed range_pos msg, true)
    3.37    end;
    3.38  
    3.39 +fun read_command pos str =
    3.40 +  let
    3.41 +    val (lexs, outer_syntax) = get_syntax ();
    3.42 +    val toks = Thy_Syntax.parse_tokens lexs pos str;
    3.43 +  in #1 (read_span outer_syntax toks) end;
    3.44 +
    3.45  fun read_element outer_syntax init {head, proof, proper_proof} =
    3.46    let
    3.47 -    val (tr, proper_head) = read_span outer_syntax head |>> Toplevel.modify_init init;
    3.48 -    val proof_trs = map (read_span outer_syntax) proof |> filter #2 |> map #1;
    3.49 +    val read = read_span outer_syntax o Thy_Syntax.span_content;
    3.50 +    val (tr, proper_head) = read head |>> Toplevel.modify_init init;
    3.51 +    val proof_trs = map read proof |> filter #2 |> map #1;
    3.52    in
    3.53      if proper_head andalso proper_proof then [(tr, proof_trs)]
    3.54      else map (rpair []) (if proper_head then tr :: proof_trs else proof_trs)
    3.55    end;
    3.56  
    3.57 -fun read_command pos str =
    3.58 -  let val (lexs, outer_syntax) = get_syntax () in
    3.59 -    (case Thy_Syntax.parse_spans lexs pos str of
    3.60 -      [span] => #1 (read_span outer_syntax span)
    3.61 -    | _ => Toplevel.malformed pos not_singleton)
    3.62 -  end;
    3.63 -
    3.64  end;
    3.65  
     4.1 --- a/src/Pure/Isar/token.ML	Fri Sep 02 19:29:48 2011 +0200
     4.2 +++ b/src/Pure/Isar/token.ML	Fri Sep 02 23:04:12 2011 +0200
     4.3 @@ -18,6 +18,7 @@
     4.4    val position_of: T -> Position.T
     4.5    val end_position_of: T -> Position.T
     4.6    val pos_of: T -> string
     4.7 +  val range: T list -> Position.range
     4.8    val eof: T
     4.9    val is_eof: T -> bool
    4.10    val not_eof: T -> bool
    4.11 @@ -122,6 +123,13 @@
    4.12  
    4.13  val pos_of = Position.str_of o position_of;
    4.14  
    4.15 +fun range [] = (Position.none, Position.none)
    4.16 +  | range toks =
    4.17 +      let
    4.18 +        val start_pos = position_of (hd toks);
    4.19 +        val end_pos = end_position_of (List.last toks);
    4.20 +      in (start_pos, end_pos) end;
    4.21 +
    4.22  
    4.23  (* control tokens *)
    4.24  
     5.1 --- a/src/Pure/PIDE/document.ML	Fri Sep 02 19:29:48 2011 +0200
     5.2 +++ b/src/Pure/PIDE/document.ML	Fri Sep 02 23:04:12 2011 +0200
     5.3 @@ -25,7 +25,6 @@
     5.4    type state
     5.5    val init_state: state
     5.6    val define_command: command_id -> string -> string -> state -> state
     5.7 -  val join_commands: state -> state
     5.8    val cancel_execution: state -> Future.task list
     5.9    val update_perspective: version_id -> version_id -> string -> command_id list -> state -> state
    5.10    val update: version_id -> version_id -> edit list -> state ->
    5.11 @@ -237,9 +236,7 @@
    5.12  
    5.13  abstype state = State of
    5.14   {versions: version Inttab.table,  (*version_id -> document content*)
    5.15 -  commands:
    5.16 -    (string * Toplevel.transition future) Inttab.table *  (*command_id -> name * transition*)
    5.17 -    Toplevel.transition future list,  (*recent commands to be joined*)
    5.18 +  commands: (string * Toplevel.transition future) Inttab.table,  (*command_id -> name * transition*)
    5.19    execs: (command_id * (Toplevel.state * unit lazy) lazy) Inttab.table,
    5.20      (*exec_id -> command_id with eval/print process*)
    5.21    execution: Future.group}  (*global execution process*)
    5.22 @@ -253,7 +250,7 @@
    5.23  
    5.24  val init_state =
    5.25    make_state (Inttab.make [(no_id, empty_version)],
    5.26 -    (Inttab.make [(no_id, (Toplevel.name_of Toplevel.empty, Future.value Toplevel.empty))], []),
    5.27 +    Inttab.make [(no_id, (Toplevel.name_of Toplevel.empty, Future.value Toplevel.empty))],
    5.28      Inttab.make [(no_id, (no_id, Lazy.value (Toplevel.toplevel, no_print)))],
    5.29      Future.new_group NONE);
    5.30  
    5.31 @@ -275,27 +272,26 @@
    5.32  (* commands *)
    5.33  
    5.34  fun define_command (id: command_id) name text =
    5.35 -  map_state (fn (versions, (commands, recent), execs, execution) =>
    5.36 +  map_state (fn (versions, commands, execs, execution) =>
    5.37      let
    5.38        val id_string = print_id id;
    5.39 -      val tr =
    5.40 -        Future.fork_pri 2 (fn () =>
    5.41 -          Position.setmp_thread_data (Position.id_only id_string)
    5.42 -            (fn () => Outer_Syntax.read_command (Position.id id_string) text) ());
    5.43 +      val future =
    5.44 +        (singleton o Future.forks)
    5.45 +          {name = "Document.define_command", group = SOME (Future.new_group NONE),
    5.46 +            deps = [], pri = ~1, interrupts = false}
    5.47 +          (fn () =>
    5.48 +            Position.setmp_thread_data (Position.id_only id_string)
    5.49 +              (fn () => Outer_Syntax.read_command (Position.id id_string) text) ());
    5.50        val commands' =
    5.51 -        Inttab.update_new (id, (name, tr)) commands
    5.52 +        Inttab.update_new (id, (name, future)) commands
    5.53            handle Inttab.DUP dup => err_dup "command" dup;
    5.54 -    in (versions, (commands', tr :: recent), execs, execution) end);
    5.55 +    in (versions, commands', execs, execution) end);
    5.56  
    5.57  fun the_command (State {commands, ...}) (id: command_id) =
    5.58 -  (case Inttab.lookup (#1 commands) id of
    5.59 +  (case Inttab.lookup commands id of
    5.60      NONE => err_undef "command" id
    5.61    | SOME command => command);
    5.62  
    5.63 -val join_commands =
    5.64 -    map_state (fn (versions, (commands, recent), execs, execution) =>
    5.65 -      (Future.join_results recent; (versions, (commands, []), execs, execution)));
    5.66 -
    5.67  
    5.68  (* command executions *)
    5.69  
    5.70 @@ -419,20 +415,16 @@
    5.71    if bad_init andalso is_none init then NONE
    5.72    else
    5.73      let
    5.74 -      val (name, tr0) = the_command state command_id';
    5.75 +      val (name, tr0) = the_command state command_id' ||> Future.join;
    5.76        val (modify_init, init') =
    5.77          if Keyword.is_theory_begin name then
    5.78            (Toplevel.modify_init (the_default illegal_init init), NONE)
    5.79          else (I, init);
    5.80 -        val exec_id' = new_id ();
    5.81 -      val exec' =
    5.82 -        snd exec |> Lazy.map (fn (st, _) =>
    5.83 -          let val tr =
    5.84 -            Future.join tr0
    5.85 -            |> modify_init
    5.86 -            |> Toplevel.put_id (print_id exec_id');
    5.87 -          in run_command tr st end)
    5.88 -        |> pair command_id';
    5.89 +      val exec_id' = new_id ();
    5.90 +      val tr = tr0
    5.91 +        |> modify_init
    5.92 +        |> Toplevel.put_id (print_id exec_id');
    5.93 +      val exec' = (command_id', Lazy.map (fn (st, _) => run_command tr st) (snd exec));
    5.94      in SOME ((exec_id', exec') :: execs, exec', init') end;
    5.95  
    5.96  fun make_required nodes =
     6.1 --- a/src/Pure/PIDE/isar_document.ML	Fri Sep 02 19:29:48 2011 +0200
     6.2 +++ b/src/Pure/PIDE/isar_document.ML	Fri Sep 02 23:04:12 2011 +0200
     6.3 @@ -55,15 +55,14 @@
     6.4          val running = Document.cancel_execution state;
     6.5          val (assignment, state1) = Document.update old_id new_id edits state;
     6.6          val _ = Future.join_tasks running;
     6.7 -        val state2 = Document.join_commands state1;
     6.8          val _ =
     6.9 -          Output.status (Markup.markup (Markup.assign new_id)
    6.10 -            (assignment |>
    6.11 +          Output.raw_message Markup.assign_execs
    6.12 +            ((new_id, assignment) |>
    6.13                let open XML.Encode
    6.14 -              in pair (list (pair int (option int))) (list (pair string (option int))) end
    6.15 -              |> YXML.string_of_body));
    6.16 -        val state3 = Document.execute new_id state2;
    6.17 -      in state3 end));
    6.18 +              in pair int (pair (list (pair int (option int))) (list (pair string (option int)))) end
    6.19 +              |> YXML.string_of_body);
    6.20 +        val state2 = Document.execute new_id state1;
    6.21 +      in state2 end));
    6.22  
    6.23  val _ =
    6.24    Isabelle_Process.add_command "Isar_Document.invoke_scala"
     7.1 --- a/src/Pure/PIDE/isar_document.scala	Fri Sep 02 19:29:48 2011 +0200
     7.2 +++ b/src/Pure/PIDE/isar_document.scala	Fri Sep 02 23:04:12 2011 +0200
     7.3 @@ -13,19 +13,16 @@
     7.4  
     7.5    object Assign
     7.6    {
     7.7 -    def unapply(msg: XML.Tree): Option[(Document.Version_ID, Document.Assign)] =
     7.8 -      msg match {
     7.9 -        case XML.Elem(Markup(Markup.ASSIGN, List((Markup.VERSION, Document.ID(id)))), body) =>
    7.10 -          try {
    7.11 -            import XML.Decode._
    7.12 -            val a = pair(list(pair(long, option(long))), list(pair(string, option(long))))(body)
    7.13 -            Some(id, a)
    7.14 -          }
    7.15 -          catch {
    7.16 -            case _: XML.XML_Atom => None
    7.17 -            case _: XML.XML_Body => None
    7.18 -          }
    7.19 -        case _ => None
    7.20 +    def unapply(text: String): Option[(Document.Version_ID, Document.Assign)] =
    7.21 +      try {
    7.22 +        import XML.Decode._
    7.23 +        val body = YXML.parse_body(text)
    7.24 +        Some(pair(long, pair(list(pair(long, option(long))), list(pair(string, option(long)))))(body))
    7.25 +      }
    7.26 +      catch {
    7.27 +        case ERROR(_) => None
    7.28 +        case _: XML.XML_Atom => None
    7.29 +        case _: XML.XML_Body => None
    7.30        }
    7.31    }
    7.32  
     8.1 --- a/src/Pure/System/session.scala	Fri Sep 02 19:29:48 2011 +0200
     8.2 +++ b/src/Pure/System/session.scala	Fri Sep 02 23:04:12 2011 +0200
     8.3 @@ -288,6 +288,13 @@
     8.4            catch {
     8.5              case _: Document.State.Fail => bad_result(result)
     8.6            }
     8.7 +        case Markup.Assign_Execs if result.is_raw =>
     8.8 +          XML.content(result.body).mkString match {
     8.9 +            case Isar_Document.Assign(id, assign) =>
    8.10 +              try { handle_assign(id, assign) }
    8.11 +              catch { case _: Document.State.Fail => bad_result(result) }
    8.12 +            case _ => bad_result(result)
    8.13 +          }
    8.14          case Markup.Invoke_Scala(name, id) if result.is_raw =>
    8.15            Future.fork {
    8.16              val arg = XML.content(result.body).mkString
    8.17 @@ -311,9 +318,6 @@
    8.18            else if (result.is_stdout) { }
    8.19            else if (result.is_status) {
    8.20              result.body match {
    8.21 -              case List(Isar_Document.Assign(id, assign)) =>
    8.22 -                try { handle_assign(id, assign) }
    8.23 -                catch { case _: Document.State.Fail => bad_result(result) }
    8.24                case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
    8.25                case List(Keyword.Keyword_Decl(name)) => syntax += name
    8.26                case List(Thy_Info.Loaded_Theory(name)) => thy_load.register_thy(name)
     9.1 --- a/src/Pure/Thy/thy_syntax.ML	Fri Sep 02 19:29:48 2011 +0200
     9.2 +++ b/src/Pure/Thy/thy_syntax.ML	Fri Sep 02 23:04:12 2011 +0200
     9.3 @@ -16,7 +16,6 @@
     9.4    type span
     9.5    val span_kind: span -> span_kind
     9.6    val span_content: span -> Token.T list
     9.7 -  val span_range: span -> Position.range
     9.8    val span_source: (Token.T, 'a) Source.source -> (span, (Token.T, 'a) Source.source) Source.source
     9.9    val parse_spans: Scan.lexicon * Scan.lexicon -> Position.T -> string -> span list
    9.10    val present_span: span -> Output.output
    9.11 @@ -101,15 +100,6 @@
    9.12  fun span_kind (Span (k, _)) = k;
    9.13  fun span_content (Span (_, toks)) = toks;
    9.14  
    9.15 -fun span_range span =
    9.16 -  (case span_content span of
    9.17 -    [] => (Position.none, Position.none)
    9.18 -  | toks =>
    9.19 -      let
    9.20 -        val start_pos = Token.position_of (hd toks);
    9.21 -        val end_pos = Token.end_position_of (List.last toks);
    9.22 -      in (start_pos, end_pos) end);
    9.23 -
    9.24  
    9.25  (* parse *)
    9.26  
    10.1 --- a/src/Tools/jEdit/src/text_area_painter.scala	Fri Sep 02 19:29:48 2011 +0200
    10.2 +++ b/src/Tools/jEdit/src/text_area_painter.scala	Fri Sep 02 23:04:12 2011 +0200
    10.3 @@ -201,6 +201,7 @@
    10.4            x + w < clip_rect.x + clip_rect.width && chunk.accessable)
    10.5        {
    10.6          val chunk_range = Text.Range(chunk_offset, chunk_offset + chunk.length)
    10.7 +        val chunk_str = if (chunk.str == null) " " * chunk.length else chunk.str
    10.8          val chunk_font = chunk.style.getFont
    10.9          val chunk_color = chunk.style.getForegroundColor
   10.10  
   10.11 @@ -229,7 +230,7 @@
   10.12          var x1 = x + w
   10.13          gfx.setFont(chunk_font)
   10.14          for (Text.Info(range, info) <- padded_markup if !range.is_singularity) {
   10.15 -          val str = chunk.str.substring(range.start - chunk_offset, range.stop - chunk_offset)
   10.16 +          val str = chunk_str.substring(range.start - chunk_offset, range.stop - chunk_offset)
   10.17            gfx.setColor(info.getOrElse(chunk_color))
   10.18  
   10.19            range.try_restrict(caret_range) match {