diff --git a/src/haz3lweb/app/editors/mode/ExercisesMode.re b/src/haz3lweb/app/editors/mode/ExercisesMode.re index 0423a29b25..29252035f2 100644 --- a/src/haz3lweb/app/editors/mode/ExercisesMode.re +++ b/src/haz3lweb/app/editors/mode/ExercisesMode.re @@ -175,8 +175,10 @@ module Update = { let export_exercise_module = (exercises: Model.t): unit => { let exercise = Model.get_current(exercises); - let module_name = exercise.editors.module_name; - let filename = exercise.editors.module_name ++ ".ml"; + let module_name = + StringUtil.isEmptyOrWhitespace(exercise.editors.module_name) + ? "Unnamed Exercise Module" : exercise.editors.module_name; + let filename = module_name ++ ".ml"; let content_type = "text/plain"; let contents = Exercise.export_module(module_name, {eds: exercise.editors}); diff --git a/src/util/StringUtil.re b/src/util/StringUtil.re index a4fedde846..3dca02e169 100644 --- a/src/util/StringUtil.re +++ b/src/util/StringUtil.re @@ -63,3 +63,8 @@ let unescape_linebreaks: string => string = Re.Str.global_replace(Re.Str.regexp("\\\\n"), "\n"); let trim_leading = Re.Str.global_replace(Re.Str.regexp("\n[ ]*"), "\n"); + +let isEmptyOrWhitespace = str => { + let trimmed = String.trim(str); + String.length(trimmed) == 0; +};