From 5fe00683010ed7e4649e8fe52cf4ea60cf4af2d2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 27 Nov 2016 19:43:26 -0800
Subject: [PATCH] feat(shell/lean): error if leandoc is used with smt2 files

---
 src/shell/lean.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp
index a2b7d1f117..c9945ac7fe 100644
--- a/src/shell/lean.cpp
+++ b/src/shell/lean.cpp
@@ -368,6 +368,7 @@ int main(int argc, char ** argv) {
     #endif
 
     environment env = mk_environment(trust_lvl);
+
     io_state ios(opts, lean::mk_pretty_formatter_factory());
 #if defined(LEAN_SERVER)
     if (json_output) {
@@ -382,6 +383,7 @@ int main(int argc, char ** argv) {
         bool ok = true;
         for (int i = optind; i < argc; i++) {
             try {
+                if (doc) throw lean::exception("leandoc does not support .smt2 files");
                 ok = ::lean::smt2::parse_commands(env, ios, argv[i]);
             } catch (lean::exception & ex) {
                 ok = false;