# HG changeset patch
# User wenzelm
# Date 1570477891 -7200
# Node ID 5352449209b11d75e65e54279947900b46fed87b
# Parent  44eeca528557277640210f625559264ea6c089e9
clarified option type;

diff -r 44eeca528557 -r 5352449209b1 etc/options
--- a/etc/options	Mon Oct 07 17:20:26 2019 +0200
+++ b/etc/options	Mon Oct 07 21:51:31 2019 +0200
@@ -222,7 +222,7 @@
 option headless_commit_cleanup_delay : real = 60
   -- "delay for cleanup of already imported theories (seconds, 0 = disabled)"
 
-option headless_load_limit : int = 5
+option headless_load_limit : real = 5.0
   -- "limit in MB for loaded theory files (0 = unlimited)"
 
 
diff -r 44eeca528557 -r 5352449209b1 src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Mon Oct 07 17:20:26 2019 +0200
+++ b/src/Pure/PIDE/headless.scala	Mon Oct 07 21:51:31 2019 +0200
@@ -271,7 +271,7 @@
             maximals.sortBy(node => - depth(node))
           }
         val load_limit =
-          if (commit.isDefined) session_options.int("headless_load_limit").toLong * 1024 * 1024
+          if (commit.isDefined) (session_options.real("headless_load_limit") * 1024 * 1024).round
           else 0
         val load_state = Load_State(Nil, rest, load_limit)