clarified define_command: send tokens more directly, without requiring keywords in ML;
authorwenzelm
Wed Dec 03 20:45:20 2014 +0100 (2014-12-03)
changeset 5908508a6901eb035
parent 59084 f982f3072d79
child 59086 94b2690ad494
clarified define_command: send tokens more directly, without requiring keywords in ML;
src/Pure/General/position.ML
src/Pure/Isar/token.ML
src/Pure/PIDE/document.ML
src/Pure/PIDE/protocol.ML
src/Pure/PIDE/protocol.scala
     1.1 --- a/src/Pure/General/position.ML	Wed Dec 03 15:22:27 2014 +0100
     1.2 +++ b/src/Pure/General/position.ML	Wed Dec 03 20:45:20 2014 +0100
     1.3 @@ -14,6 +14,7 @@
     1.4    val end_offset_of: T -> int option
     1.5    val file_of: T -> string option
     1.6    val advance: Symbol.symbol -> T -> T
     1.7 +  val advance_offset: int -> T -> T
     1.8    val distance_of: T -> T -> int
     1.9    val none: T
    1.10    val start: T
    1.11 @@ -101,6 +102,11 @@
    1.12  fun advance sym (pos as (Pos (count, props))) =
    1.13    if invalid_count count then pos else Pos (advance_count sym count, props);
    1.14  
    1.15 +fun advance_offset offset (pos as (Pos (count as (i, j, k), props))) =
    1.16 +  if invalid_count count then pos
    1.17 +  else if valid i then raise Fail "Illegal line position"
    1.18 +  else Pos ((i, if_valid j (j + offset), k), props);
    1.19 +
    1.20  
    1.21  (* distance of adjacent positions *)
    1.22  
     2.1 --- a/src/Pure/Isar/token.ML	Wed Dec 03 15:22:27 2014 +0100
     2.2 +++ b/src/Pure/Isar/token.ML	Wed Dec 03 20:45:20 2014 +0100
     2.3 @@ -90,6 +90,7 @@
     2.4      Position.T -> (Symbol.symbol, 'a) Source.source -> (T,
     2.5        (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
     2.6    val explode: Keyword.keywords -> Position.T -> string -> T list
     2.7 +  val make: (int * int) * string -> Position.T -> T * Position.T
     2.8    type 'a parser = T list -> 'a * T list
     2.9    type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list)
    2.10    val read_no_commands: Keyword.keywords -> 'a parser -> Symbol_Pos.T list -> 'a list
    2.11 @@ -135,6 +136,10 @@
    2.12    | Error _ => "bad input"
    2.13    | EOF => "end-of-input";
    2.14  
    2.15 +val immediate_kinds =
    2.16 +  Vector.fromList
    2.17 +    [Command, Keyword, Ident, Long_Ident, Sym_Ident, Var, Type_Ident, Type_Var, Nat, Float, Space];
    2.18 +
    2.19  val delimited_kind = member (op =) [String, Alt_String, Verbatim, Cartouche, Comment];
    2.20  
    2.21  
    2.22 @@ -591,6 +596,22 @@
    2.23    Source.exhaust;
    2.24  
    2.25  
    2.26 +(* make *)
    2.27 +
    2.28 +fun make ((k, n), s) pos =
    2.29 +  let
    2.30 +    val pos' = Position.advance_offset n pos;
    2.31 +    val range = Position.range pos pos';
    2.32 +    val tok =
    2.33 +      if k < Vector.length immediate_kinds then
    2.34 +        Token ((s, range), (Vector.sub (immediate_kinds, k), s), Slot)
    2.35 +      else
    2.36 +        (case explode Keyword.empty_keywords pos s of
    2.37 +          [tok] => tok
    2.38 +        | _ => Token ((s, range), (Error (err_prefix ^ "exactly one token expected"), s), Slot))
    2.39 +  in (tok, pos') end;
    2.40 +
    2.41 +
    2.42  
    2.43  (** parsers **)
    2.44  
     3.1 --- a/src/Pure/PIDE/document.ML	Wed Dec 03 15:22:27 2014 +0100
     3.2 +++ b/src/Pure/PIDE/document.ML	Wed Dec 03 20:45:20 2014 +0100
     3.3 @@ -20,8 +20,8 @@
     3.4    val init_state: state
     3.5    val define_blob: string -> string -> state -> state
     3.6    type blob_digest = (string * string option) Exn.result
     3.7 -  val define_command: Document_ID.command -> string -> blob_digest list -> string ->
     3.8 -    state -> state
     3.9 +  val define_command: Document_ID.command -> string -> blob_digest list ->
    3.10 +    ((int * int) * string) list -> state -> state
    3.11    val remove_versions: Document_ID.version list -> state -> state
    3.12    val start_execution: state -> state
    3.13    val update: Document_ID.version -> Document_ID.version -> edit list -> state ->
    3.14 @@ -326,14 +326,14 @@
    3.15  
    3.16  (* commands *)
    3.17  
    3.18 -fun define_command command_id name command_blobs text =
    3.19 +fun define_command command_id name command_blobs toks =
    3.20    map_state (fn (versions, blobs, commands, execution) =>
    3.21      let
    3.22        val id = Document_ID.print command_id;
    3.23        val span =
    3.24          Lazy.lazy (fn () =>
    3.25            Position.setmp_thread_data (Position.id_only id)
    3.26 -            (fn () => Token.explode (get_keywords ()) (Position.id id) text) ());
    3.27 +            (fn () => #1 (fold_map Token.make toks (Position.id id))) ());
    3.28        val _ =
    3.29          Position.setmp_thread_data (Position.id_only id)
    3.30            (fn () => Output.status (Markup.markup_only Markup.accepted)) ();
     4.1 --- a/src/Pure/PIDE/protocol.ML	Wed Dec 03 15:22:27 2014 +0100
     4.2 +++ b/src/Pure/PIDE/protocol.ML	Wed Dec 03 20:45:20 2014 +0100
     4.3 @@ -32,7 +32,7 @@
     4.4  
     4.5  val _ =
     4.6    Isabelle_Process.protocol_command "Document.define_command"
     4.7 -    (fn [id, name, blobs_yxml, text] =>
     4.8 +    (fn id :: name :: blobs_yxml :: toks_yxml :: sources =>
     4.9        let
    4.10          val blobs =
    4.11            YXML.parse_body blobs_yxml |>
    4.12 @@ -41,8 +41,10 @@
    4.13                 [fn ([], a) => Exn.Res (pair string (option string) a),
    4.14                  fn ([], a) => Exn.Exn (ERROR (string a))])
    4.15              end;
    4.16 +        val toks =
    4.17 +          (YXML.parse_body toks_yxml |> let open XML.Decode in list (pair int int) end) ~~ sources;
    4.18        in
    4.19 -        Document.change_state (Document.define_command (Document_ID.parse id) name blobs text)
    4.20 +        Document.change_state (Document.define_command (Document_ID.parse id) name blobs toks)
    4.21        end);
    4.22  
    4.23  val _ =
     5.1 --- a/src/Pure/PIDE/protocol.scala	Wed Dec 03 15:22:27 2014 +0100
     5.2 +++ b/src/Pure/PIDE/protocol.scala	Wed Dec 03 20:45:20 2014 +0100
     5.3 @@ -392,10 +392,21 @@
     5.4            { case Exn.Res((a, b)) =>
     5.5                (Nil, pair(string, option(string))((a.node, b.map(p => p._1.toString)))) },
     5.6            { case Exn.Exn(e) => (Nil, string(Exn.message(e))) }))
     5.7 +
     5.8        YXML.string_of_body(list(encode_blob)(command.blobs))
     5.9      }
    5.10 +
    5.11 +    val toks = command.span.content
    5.12 +    val toks_yxml =
    5.13 +    { import XML.Encode._
    5.14 +      val encode_tok: T[Token] =
    5.15 +        (tok => pair(int, int)((tok.kind.id, Symbol.iterator(tok.source).length)))
    5.16 +      YXML.string_of_body(list(encode_tok)(toks))
    5.17 +    }
    5.18 +
    5.19      protocol_command("Document.define_command",
    5.20 -      Document_ID(command.id), encode(command.name), blobs_yxml, encode(command.source))
    5.21 +      (Document_ID(command.id) :: encode(command.name) :: blobs_yxml :: toks_yxml ::
    5.22 +        toks.map(tok => encode(tok.source))): _*)
    5.23    }
    5.24  
    5.25