Changes for new webinterface

Isabelle/Isabelle.cabal

@@ -0,0 +1,53 @@
+cabal-version: 1.12
+
+-- This file has been generated from package.yaml by hpack version 0.34.4.
+--
+-- see: https://github.com/sol/hpack
+
+name:           Isabelle
+version:        0.1.0.0
+description:    <https://github.com/naproche/naproche>
+homepage:       https://github.com/naproche/naproche#readme
+bug-reports:    https://github.com/naproche/naproche/issues
+license:        GPL-3
+build-type:     Simple
+
+source-repository head
+  type: git
+  location: https://github.com/naproche/naproche
+
+library
+  exposed-modules:
+      Isabelle.Server
+      Isabelle.Byte_Message
+      Isabelle.Isabelle_System
+  other-modules:
+      Paths_Isabelle
+  hs-source-dirs:
+      src
+  default-extensions:
+      GeneralizedNewtypeDeriving
+      InstanceSigs
+      LambdaCase
+      PartialTypeSignatures
+      ScopedTypeVariables
+  ghc-options: -O2 -Wall -fno-warn-unused-do-bind -fno-warn-unused-matches -fno-warn-name-shadowing
+  build-depends:
+      Naproche-SAD
+    , array
+    , base >=4.7 && <5
+    , bytestring
+    , containers
+    , ghc-prim
+    , megaparsec
+    , mtl
+    , network
+    , process
+    , split
+    , temporary
+    , text
+    , threads
+    , time
+    , transformers
+    , uuid
+  default-language: Haskell2010

Isabelle/package.yaml

@@ -0,0 +1,47 @@
+name:                Isabelle 
+version:             0.1.0.0
+github:              "naproche/naproche"
+license:             GPL-3
+
+description:         <https://github.com/naproche/naproche>
+
+dependencies:
+- base >= 4.7 && < 5
+- array
+- bytestring
+- containers
+- ghc-prim
+- megaparsec
+- mtl
+- network
+- process
+- split
+- temporary
+- text
+- threads
+- time
+- transformers
+- uuid
+- Naproche-SAD
+
+default-extensions:
+  - GeneralizedNewtypeDeriving
+  - InstanceSigs
+  - LambdaCase
+  - PartialTypeSignatures
+  - ScopedTypeVariables
+
+ghc-options:
+  - -O2
+  - -Wall
+  - -fno-warn-unused-do-bind
+  - -fno-warn-unused-matches
+  - -fno-warn-name-shadowing
+
+library:
+  source-dirs:
+    - src
+  exposed-modules:
+    - Isabelle.Server
+    - Isabelle.Byte_Message
+    - Isabelle.Isabelle_System

app/naproche.cabal

@@ -0,0 +1,87 @@
+cabal-version: 1.12
+
+-- This file has been generated from package.yaml by hpack version 0.34.4.
+--
+-- see: https://github.com/sol/hpack
+
+name:           naproche
+version:        0.1.0.0
+description:    <https://github.com/naproche/naproche>
+homepage:       https://github.com/naproche/naproche#readme
+bug-reports:    https://github.com/naproche/naproche/issues
+license:        GPL-3
+build-type:     Simple
+
+source-repository head
+  type: git
+  location: https://github.com/naproche/naproche
+
+executable Naproche-SAD
+  main-is: Main.hs
+  other-modules:
+      PIDE
+      Paths_naproche
+  hs-source-dirs:
+      src
+  default-extensions:
+      GeneralizedNewtypeDeriving
+      InstanceSigs
+      LambdaCase
+      PartialTypeSignatures
+      ScopedTypeVariables
+  ghc-options: -O2 -Wall -fno-warn-unused-do-bind -fno-warn-unused-matches -fno-warn-name-shadowing -threaded -rtsopts -with-rtsopts=-N
+  build-depends:
+      Isabelle
+    , Naproche-SAD
+    , array
+    , base >=4.7 && <5
+    , bytestring
+    , containers
+    , ghc-prim
+    , megaparsec
+    , mtl
+    , network
+    , process
+    , split
+    , temporary
+    , text
+    , threads
+    , time
+    , transformers
+    , uuid
+  default-language: Haskell2010
+
+test-suite Naproche-SAD-test
+  type: exitcode-stdio-1.0
+  main-is: Spec.hs
+  other-modules:
+      Paths_naproche
+  hs-source-dirs:
+      test
+  default-extensions:
+      GeneralizedNewtypeDeriving
+      InstanceSigs
+      LambdaCase
+      PartialTypeSignatures
+      ScopedTypeVariables
+  ghc-options: -O2 -Wall -fno-warn-unused-do-bind -fno-warn-unused-matches -fno-warn-name-shadowing -threaded -rtsopts -with-rtsopts=-N
+  build-depends:
+      Isabelle
+    , Naproche-SAD
+    , array
+    , base >=4.7 && <5
+    , bytestring
+    , containers
+    , ghc-prim
+    , megaparsec
+    , mtl
+    , network
+    , process
+    , split
+    , temporary
+    , text
+    , threads
+    , time
+    , transformers
+    , uuid
+  default-language: Haskell2010

package.yaml → app/package.yaml

@@ -1,29 +1,9 @@
-name:                Naproche-SAD
+name:                naproche
 version:             0.1.0.0
-github:              "naproche-community/naproche"
+github:              "naproche/naproche"
 license:             GPL-3
 
-extra-source-files:
-- README.md
-
-description:         <https://github.com/naproche-community/naproche>
-
-flags:
-  debug:
-    description: "Enable special debugging support"
-    manual: true
-    default: false
-
-
-when:
-  condition: flag(debug)
-  dependencies:
-  - haskell-stack-trace-plugin
-  ghc-options:
-  - -fplugin=StackTrace.Plugin
-  - -Weverything
-  - -Wno-unsafe
-  - -Wno-implicit-prelude
+description:         <https://github.com/naproche/naproche>
 
 dependencies:
 - base >= 4.7 && < 5
@@ -42,6 +22,8 @@ dependencies:
 - time
 - transformers
 - uuid
+- Naproche-SAD
+- Isabelle
 
 default-extensions:
   - GeneralizedNewtypeDeriving
@@ -57,29 +39,10 @@ ghc-options:
   - -fno-warn-unused-matches
   - -fno-warn-name-shadowing
 
-library:
-  source-dirs:
-    - src
-    - Isabelle/src
-  exposed-modules:
-    - Isabelle.File
-    - Isabelle.Server
-    - Isabelle.Byte_Message
-    - Isabelle.Properties
-    - Isabelle.UTF8
-    - Isabelle.XML
-    - Isabelle.YXML
-    - Isabelle.UUID
-    - Isabelle.Isabelle_Thread
-    - Isabelle.Library
-    - Isabelle.Naproche
-    - SAD.API
-    - SAD.Main
-
 executables:
   Naproche-SAD:
     main:                Main.hs
-    source-dirs:         app
+    source-dirs:         src
     ghc-options:
     - -threaded
     - -rtsopts

app/src/Main.hs

@@ -0,0 +1,123 @@
+{-# LANGUAGE OverloadedStrings #-}
+{-# OPTIONS_GHC -Wno-orphans #-}
+
+module Main where
+
+import Control.Monad (when)
+import Data.Maybe (mapMaybe)
+
+import qualified Control.Exception as Exception
+import Control.Exception (catch)
+import qualified Data.Text.Lazy as Text
+import qualified System.Console.GetOpt as GetOpt
+import qualified System.Environment as Environment
+import Network.Socket (Socket)
+
+import qualified Isabelle.Byte_Message as Byte_Message
+import qualified Isabelle.Naproche as Naproche
+import qualified Isabelle.Server as Server
+import qualified Isabelle.Options as Options
+import qualified Isabelle.Isabelle_Thread as Isabelle_Thread
+import qualified Isabelle.UUID as UUID
+import qualified Isabelle.Position as Position
+import qualified Isabelle.YXML as YXML
+import qualified Isabelle.Process_Result as Process_Result
+import qualified Isabelle.File
+import Isabelle.Library
+
+import SAD.Data.Instr
+import qualified SAD.Core.Message as Message
+import SAD.API
+
+import qualified Naproche.Program as Program
+import qualified Naproche.Console as Console
+import qualified Naproche.File as File
+
+import qualified SAD.Main
+import qualified PIDE
+import System.IO.Error (ioeGetErrorString)
+
+main :: IO ()
+main  = do
+  Console.setup
+
+  -- command line and init file
+  args0 <- Environment.getArgs
+  (opts0, pk, fileArg) <- SAD.Main.readArgs args0
+  text0 <- (map (uncurry ProofTextInstr) (reverse opts0) ++) <$> case fileArg of
+    Nothing -> do
+      stdin <- getContents
+      pure [ProofTextInstr Position.none $ GetArgument (Text pk) (Text.pack stdin)]
+    Just name -> do
+      pure [ProofTextInstr Position.none $ GetArgument (File pk) (Text.pack name)]
+  let opts1 = map snd opts0
+
+  if getInstr helpParam opts1 then
+    putStr (GetOpt.usageInfo SAD.Main.usageHeader SAD.Main.options)
+  else -- main body with explicit error handling, notably for PIDE
+      (if getInstr serverParam opts1 then
+        Server.server (Server.publish_stdout "Naproche-SAD") (mainServer args0)
+      else do
+        Program.init_console
+        rc <- do
+          SAD.Main.mainBody opts1 text0 fileArg
+            `catch` (\Exception.UserInterrupt -> do
+              Program.exit_thread
+              Console.stderr ("Interrupt" :: String)
+              return Process_Result.interrupt_rc)
+            `catch` (\(err :: Exception.SomeException) -> do
+              Program.exit_thread
+              Console.stderr (Exception.displayException err)
+              return 1)
+        Console.exit rc)
+
+mainServer :: [String] -> Socket -> IO ()
+mainServer args0 socket =
+  let
+    exchange_message0 = Byte_Message.exchange_message0 socket
+    robust_error msg =
+      exchange_message0 [Naproche.output_error_command, msg]
+        `catch` (\(_ :: Exception.IOException) -> return ())
+  in
+    do
+      chunks <- Byte_Message.read_message socket
+      case chunks of
+        Just (command : threads) | command == Naproche.cancel_program ->
+          mapM_ Isabelle_Thread.stop_uuid (mapMaybe UUID.parse threads)
+
+        Just [command, more_args, opts, text] | command == Naproche.forthel_program -> do
+          let options = Options.decode $ YXML.parse_body opts
+
+          Exception.bracket_ (PIDE.init_pide socket options)
+            Program.exit_thread
+            (do
+              thread_uuid <- Isabelle_Thread.my_uuid
+              mapM_ (\uuid -> exchange_message0 [Naproche.threads_command, UUID.print uuid]) thread_uuid
+
+              let more_text = Text.pack $ make_string text
+
+              (opts0, pk, fileArg) <- SAD.Main.readArgs (args0 ++ lines (make_string more_args))
+              let opts1 = map snd opts0
+              let text0 = map (uncurry ProofTextInstr) (reverse opts0)
+              let text1 = text0 ++ [ProofTextInstr Position.none (GetArgument (Text pk) more_text)]
+
+              rc <- do
+                SAD.Main.mainBody opts1 text1 fileArg
+                  `catch` (\(err :: Program.Error) -> do
+                    robust_error $ Program.print_error err
+                    return 0)
+                  `catch` (\(err :: Exception.SomeException) -> do
+                    robust_error $ make_bytes $ Exception.displayException err
+                    return 0)
+
+              when (rc /= 0) $ robust_error "ERROR")
+
+        _ -> return ()
+
+instance File.MonadFile IO where
+  read f = catch (Isabelle.File.read f)
+    (Message.errorParser (Position.file_only $ make_bytes f) . make_bytes . ioeGetErrorString)
+  write f b = catch (Isabelle.File.write f b)
+    (Message.errorParser (Position.file_only $ make_bytes f) . make_bytes . ioeGetErrorString)
+  append f b = catch (Isabelle.File.append f b)
+    (Message.errorParser (Position.file_only $ make_bytes f) . make_bytes . ioeGetErrorString)