Separate data and control in the interactive protocol

Apart from using JSON messages, the new protocol is essentially the same as the
old one.  Significant differences:

- Instead of crashing, invalid requests (missing fields, unsupported queries,
  etc) now cause F* to print a reasonably helpful diagnostic message.
- Each query now includes an editor-supplied query id, and each response
  contains the id of the corresponding query.
- Some of the queries were renamed (info → lookup, completions → autocomplete)
  for consistency (all query names are now verbs).
- Messages that F* used to print to stdout or stderr are now translated into
  proper JSON messages and labeled with a severity level (a review of these
  messages is needed to decide which of these should be turned into properly
  reported errors or warnings including range information).
- F* now prints the protocol's version and a list of supported interactive
  features before starting the interactive loop.  This lets the Emacs mode do
  dynamic capability detection instead of relying on version numbers. The same
  information is available through a new "describe-protocol" query.
- A failed “push” doesn't require the editor to immediately send a corresponding
  “pop” any more — instead, the pop happens automatically.

Fixes #361, #366, and #828.

src/basic/ml/FStar_Util.ml

@@ -359,6 +359,7 @@ let default_printer =
 let current_printer = ref default_printer
 let set_printer printer = current_printer := printer
 
+let print_raw s = pr "%s" s; flush stdout
 let print_string s = (!current_printer).printer_prinfo s
 let print_any s = (!current_printer).printer_prinfo (Marshal.to_string s [])
 let strcat s1 s2 = s1 ^ s2
@@ -528,6 +529,8 @@ let rec find_map l f =
      | None -> find_map tl f
      | y -> y
 
+let try_find f l = try Some (List.find f l) with Not_found -> None
+
 let try_find_index f l =
   let rec aux i = function
     | [] -> None

src/basic/util.fs

@@ -341,6 +341,7 @@ let default_printer =
 let current_printer = ref default_printer
 let set_printer printer = current_printer := printer
 
+let print_raw s = pr "%s" s
 let print_string s = (!current_printer).printer_prinfo s
 let print_any s = print_string (spr "%A" s)
 let strcat s1 s2 = s1 ^ s2
@@ -477,6 +478,8 @@ let find_opt f l =
     | hd::tl -> if f hd then Some hd else aux tl in
     aux l
 
+let try_find f l = List.tryFind f l
+
 let try_find_index f l = List.tryFindIndex f l
 
 let sort_with f l = List.sortWith f l

src/basic/util.fsi

@@ -139,6 +139,7 @@ type printer = {
 val default_printer : printer
 val set_printer : printer -> unit
 
+val print_raw : string -> unit
 val print_string : string -> unit
 val print_any : 'a -> unit
 val strcat : string -> string -> string
@@ -237,6 +238,7 @@ val sort_with: ('a -> 'a -> int) -> list<'a> -> list<'a>
 val set_eq: ('a -> 'a -> int) -> list<'a> -> list<'a> -> bool
 val remove_dups: ('a -> 'a -> bool) -> list<'a> -> list<'a>
 val add_unique: ('a -> 'a -> bool) -> 'a -> list<'a> -> list<'a>
+val try_find: ('a -> bool) -> list<'a> -> option<'a>
 val try_find_i: (int -> 'a -> bool) -> list<'a> -> option<(int * 'a)>
 val find_map: list<'a> -> ('a -> option<'b>) -> option<'b>
 val try_find_index: ('a -> bool) -> list<'a> -> option<int>