From e7427d5c67c0a90c369adecb4b0c65c043cb2e34 Mon Sep 17 00:00:00 2001
From: stuebinm
Date: Tue, 26 Oct 2021 18:13:50 +0200
Subject: actually usable code structure for isabelle-proto

---
 isabelle-proto/src/main.rs | 91 +---------------------------------------------
 1 file changed, 2 insertions(+), 89 deletions(-)

(limited to 'isabelle-proto/src/main.rs')

diff --git a/isabelle-proto/src/main.rs b/isabelle-proto/src/main.rs
index 535dd52..1b52e27 100644
--- a/isabelle-proto/src/main.rs
+++ b/isabelle-proto/src/main.rs
@@ -1,104 +1,17 @@
 
 mod session;
 mod messages;
+mod pipe;
+
 
-use regex::Regex;
-use serde::{Deserialize, Serialize, de::DeserializeOwned};
-use serde_json::{Result, Value};
 use session::IsabelleSession;
-use messages::*;
 
 
-use std::{io::{BufRead, BufReader, BufWriter, Write}, path::PathBuf, process::{ChildStdout, Command, Stdio}};
-use std::fmt::Debug;
 
 
 use structopt::StructOpt;
 
 
-fn decode_sync<'a, T> (msg: &'a str) -> Option<SyncAnswer<T, String>>
-where T: Deserialize<'a> {
-    let regex = Regex::new(r"^[a-zA-Z]+\b").unwrap();
-    let mat = regex.find(msg)?;
-    let ty = &msg[..mat.end()];
-    let rest = &msg[mat.end()..];
-
-    match ty {
-        "OK" => Some(SyncAnswer::Ok(serde_json::from_str(&rest).ok()?)),
-        "ERROR" => Some(SyncAnswer::Error(rest.to_owned())),
-        _ => None
-    }
-}
-
-fn decode_async<'a,T,E,N> (msg: &'a str) -> Option<AsyncAnswer<T,E,N>>
-where T: Deserialize<'a>, N: Deserialize<'a>, E: Deserialize<'a> {
-    let regex = Regex::new(r"^[a-zA-Z]+\b").unwrap();
-    let mat = regex.find(msg)?;
-    let ty = &msg[..mat.end()];
-    let rest = &msg[mat.end()..];
-
-    match ty {
-        "NOTE" => Some(AsyncAnswer::Note(serde_json::from_str(&rest).ok()?)),
-        "FINISHED" => Some(AsyncAnswer::Finished(serde_json::from_str(&rest).ok()?)),
-        "FAILED" => Some(AsyncAnswer::Failed(serde_json::from_str(&rest).ok()?)),
-        _ => None
-    }
-}
-
-
-
-
-fn wait_for_client(pipe: &mut BufReader<ChildStdout>) -> Option<ClientHello> {
-    for res in pipe.lines() {
-        match res {
-            Err(_) => (),
-            Ok(line) => {
-                let hello : Option<SyncAnswer<ClientHello, _>> = decode_sync(&line);
-                if let Some(SyncAnswer::Ok(data)) = hello {
-                    return Some(data);
-                }
-            }
-        }
-    }
-    None
-}
-
-
-fn wait_for_async_task<'a,T,E,N,F>
-    (reader: &mut BufReader<ChildStdout>, task: &str, mut prog: F) -> Option<T>
-where T: DeserializeOwned, E: DeserializeOwned + Debug, N: DeserializeOwned,
-F: FnMut(N)
-{
-    for res in reader.lines() {
-        match res {
-            Err(_) => (),
-            Ok(line) => {
-                let regex = Regex::new(r"^[0-9]+$").unwrap();
-                if regex.is_match(&line) {
-
-                } else {
-                    match decode_async::<T,E,N>(&line)? {
-                        AsyncAnswer::Finished(data)
-                            => return Some(data),
-                        AsyncAnswer::Failed(failed)
-                            => panic!("building session failed: {:?}", failed),
-                        AsyncAnswer::Note(val) => prog(val)
-                    }
-                }
-            }
-        }
-    };
-    None
-}
-
-fn get_async_task_id (reader: &mut BufReader<ChildStdout>) -> TaskID {
-    let mut res = String::new();
-    reader.read_line(&mut res).unwrap();
-    match decode_sync(&res).unwrap() {
-        SyncAnswer::Ok(AsyncStartOk { task }) => task,
-        SyncAnswer::Error(_) => panic!("failed to start async task!")
-    }
-}
 
 #[derive(StructOpt)]
 #[structopt(name = "isabelle-proto-POC", about="proof of concept for communicating with an Isabelle server")]
-- 
cgit v1.2.3